Avoid output duplication because of FILE* buffers

FILE* buffers are duplicated when fork()ing, and at program exit(), the C
library flushes the FILE* buffers, resulting in duplicated output.

To avoid this we flush all FILE* buffers before fork()ing.

diff --git a/rt/gc/cdgc/gc.d b/rt/gc/cdgc/gc.d
index 2d75813021e6eb0ce5d6d779cb4609000d96eb41..96c6a86360d24277f0456ea9038f17580f90864d 100644 (file)
--- a/rt/gc/cdgc/gc.d
+++ b/rt/gc/cdgc/gc.d
@@ -50,6 +50,7 @@ import opts = rt.gc.cdgc.opts;
 
 import cstdlib = tango.stdc.stdlib;
 import cstring = tango.stdc.string;
+import cstdio = tango.stdc.stdio;
 
 /*
  * This is a small optimization that proved it's usefulness. For small chunks
@@ -786,6 +787,7 @@ size_t fullcollect(void *stackTop)
     gc.stats.world_stopped();
 
     if (opts.options.fork) {
+        cstdio.fflush(null); // avoid duplicated FILE* output
         os.pid_t child_pid = os.fork();
         assert (child_pid != -1); // don't accept errors in non-release mode
         switch (child_pid) {