# HG changeset patch
# User wenzelm
# Date 1535993251 -7200
# Node ID e63eaae131655e9488205eed32799eab3339b682
# Parent  cca4555f412d2d157b69d2ac6852c695c6dae595
more robust default options, notably for node consolidation;

diff -r cca4555f412d -r e63eaae13165 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Sep 03 18:45:03 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Sep 03 18:47:31 2018 +0200
@@ -80,7 +80,7 @@
 
   def make_options(options: Options, aspects: List[Aspect]): Options =
   {
-    val options1 = options + "completion_limit=0" + "ML_statistics=false"
+    val options1 = options + "completion_limit=0" + "ML_statistics=false" + "parallel_proofs=0"
     (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
   }