changeset 70624 | 06052394efbe |
parent 70623 | 44090b702e11 |
child 70626 | cb83a582bf0c |
--- 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)(_ + _) }) }