dummy fork to produce ML_statistics even in sequential mode (e.g. for heap size);
authorwenzelm
Sun Dec 18 15:53:27 2016 +0100 (2016-12-18)
changeset 6459980ef54198f44
parent 64598 476e89d06272
child 64600 86e2f2208a58
dummy fork to produce ML_statistics even in sequential mode (e.g. for heap size);
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/Tools/build.ML	Sun Dec 18 15:41:23 2016 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Sun Dec 18 15:53:27 2016 +0100
     1.3 @@ -109,6 +109,7 @@
     1.4        (if Options.bool options "checkpoint" then ML_Heap.share_common_data () else ();
     1.5          Options.set_default options;
     1.6          Isabelle_Process.init_options ();
     1.7 +        Future.fork I;
     1.8          (Thy_Info.use_theories {
     1.9            document = Present.document_enabled (Options.string options "document"),
    1.10            symbols = symbols,