proper "editor_tracing_messages=0" as in "isabelle dump";
authorwenzelm
Fri, 03 Apr 2020 20:31:55 +0200
changeset 71679 eeaa4021f080
parent 71678 6fff34b5293e
child 71680 e20e117c3735
proper "editor_tracing_messages=0" as in "isabelle dump";
src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Apr 03 20:29:54 2020 +0200
+++ b/src/Pure/Tools/build.scala	Fri Apr 03 20:31:55 2020 +0200
@@ -477,7 +477,11 @@
     selection: Sessions.Selection = Sessions.Selection.empty): Results =
   {
     val build_options =
-      options + "pide_reports=false" + "completion_limit=0" + "ML_statistics"
+      options +
+        "ML_statistics" +
+        "completion_limit=0" +
+        "editor_tracing_messages=0" +
+        "pide_reports=false"
 
     val store = Sessions.store(build_options)