--- a/src/Pure/Tools/dump.scala Wed Aug 28 00:08:14 2019 +0200
+++ b/src/Pure/Tools/dump.scala Wed Aug 28 10:13:32 2019 +0200
@@ -203,8 +203,12 @@
{
val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
val options1 =
- options0 + "completion_limit=0" + "ML_statistics=false" +
- "parallel_proofs=0" + "editor_tracing_messages=0" + "editor_presentation"
+ options0 +
+ "completion_limit=0" +
+ "ML_statistics=false" +
+ "parallel_proofs=0" +
+ "editor_tracing_messages=0" +
+ "editor_presentation"
(options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
}