author | wenzelm |
Wed, 28 Aug 2019 10:18:50 +0200 | |
changeset 70624 | 06052394efbe |
parent 70623 | 44090b702e11 |
child 70625 | 1ae987cc052f |
--- 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)(_ + _) }) }