# HG changeset patch
# User wenzelm
# Date 1482072807 -3600
# Node ID 80ef54198f449ebf262955f8fd99a8250645e080
# Parent  476e89d0627246417cd9e3c52ba1b116827adedc
dummy fork to produce ML_statistics even in sequential mode (e.g. for heap size);

diff -r 476e89d06272 -r 80ef54198f44 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sun Dec 18 15:41:23 2016 +0100
+++ b/src/Pure/Tools/build.ML	Sun Dec 18 15:53:27 2016 +0100
@@ -109,6 +109,7 @@
       (if Options.bool options "checkpoint" then ML_Heap.share_common_data () else ();
         Options.set_default options;
         Isabelle_Process.init_options ();
+        Future.fork I;
         (Thy_Info.use_theories {
           document = Present.document_enabled (Options.string options "document"),
           symbols = symbols,