# 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,