# HG changeset patch
# User wenzelm
# Date 1585938715 -7200
# Node ID eeaa4021f080e568a854eb0fedf8833cd5d6c4c9
# Parent  6fff34b5293ea82bc2b1e0c93da3756c28f09802
proper "editor_tracing_messages=0" as in "isabelle dump";

diff -r 6fff34b5293e -r eeaa4021f080 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)