# HG changeset patch
# User wenzelm
# Date 1585938594 -7200
# Node ID 6fff34b5293ea82bc2b1e0c93da3756c28f09802
# Parent  ff2c26b8ffb1c13fe56cabf08cf18fc76b959e92
tuned;

diff -r ff2c26b8ffb1 -r 6fff34b5293e src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Fri Apr 03 20:27:52 2020 +0200
+++ b/src/Pure/Tools/dump.scala	Fri Apr 03 20:29:54 2020 +0200
@@ -106,9 +106,9 @@
         val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
         val options1 =
           options0 +
-            "completion_limit=0" +
             "ML_statistics=false" +
             "parallel_proofs=0" +
+            "completion_limit=0" +
             "editor_tracing_messages=0" +
             "editor_presentation"
         (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })