# HG changeset patch
# User wenzelm
# Date 1569954090 -7200
# Node ID 97b168f0c3a3fea639214d6f1d9177b06f231e8b
# Parent  f326596f5752ff9f9a1adae8a430eb5974716871
avoid censorship of options, e.g. relevant for Isabelle/MMT to provide its own value;

diff -r f326596f5752 -r 97b168f0c3a3 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue Oct 01 19:54:42 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Tue Oct 01 20:21:30 2019 +0200
@@ -126,7 +126,6 @@
           "ML_statistics=false" +
           "parallel_proofs=0" +
           "editor_tracing_messages=0" +
-          "editor_consolidate_delay=10" +
           "editor_presentation"
       (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
     }