# HG changeset patch
# User wenzelm
# Date 1566980012 -7200
# Node ID 44090b702e1101891050bc4db527004acb34e2c9
# Parent  f95193669ad7e0feefd5ea4fc43ea36c666277c5
tuned whitespace;

diff -r f95193669ad7 -r 44090b702e11 src/Pure/Tools/dump.scala
--- 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)(_ + _) })
   }