changeset 76471 | 1f0b2d7298d9 |
parent 76426 | b7fbe0999c17 |
child 76852 | 2915740fce1f |
--- a/src/Pure/Tools/dump.scala Sun Nov 06 12:54:46 2022 +0100 +++ b/src/Pure/Tools/dump.scala Sun Nov 06 15:28:56 2022 +0100 @@ -102,7 +102,6 @@ options0 + "parallel_proofs=0" + "completion_limit=0" + - "pide_presentation" + "editor_tracing_messages=0" aspects.foldLeft(options1) { case (opts, aspect) => aspect.options.foldLeft(opts)(_ + _) } }