more scalable -- less ML heap requirements;
authorwenzelm
Wed, 28 Aug 2019 10:18:50 +0200
changeset 70814 06052394efbe
parent 70813 44090b702e11
child 70815 1ae987cc052f
more scalable -- less ML heap requirements;
src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Wed Aug 28 10:13:32 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Wed Aug 28 10:18:50 2019 +0200
@@ -208,7 +208,8 @@
         "ML_statistics=false" +
         "parallel_proofs=0" +
         "editor_tracing_messages=0" +
-        "editor_presentation"
+        "editor_presentation" +
+        "execution_eager"
     (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
   }