# HG changeset patch
# User wenzelm
# Date 1566980330 -7200
# Node ID 06052394efbe980f79ef3e8e9a2abedb27c5dc1c
# Parent  44090b702e1101891050bc4db527004acb34e2c9
more scalable -- less ML heap requirements;

diff -r 44090b702e11 -r 06052394efbe 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)(_ + _) })
   }