changeset 76426 | b7fbe0999c17 |
parent 75394 | 42267c650205 |
child 76471 | 1f0b2d7298d9 |
--- a/src/Pure/Tools/dump.scala Fri Nov 04 11:38:01 2022 +0100 +++ b/src/Pure/Tools/dump.scala Fri Nov 04 13:33:04 2022 +0100 @@ -102,8 +102,8 @@ options0 + "parallel_proofs=0" + "completion_limit=0" + - "editor_tracing_messages=0" + - "editor_presentation" + "pide_presentation" + + "editor_tracing_messages=0" aspects.foldLeft(options1) { case (opts, aspect) => aspect.options.foldLeft(opts)(_ + _) } }