author | wenzelm |
Fri, 03 Apr 2020 20:31:55 +0200 | |
changeset 71679 | eeaa4021f080 |
parent 71678 | 6fff34b5293e |
child 71680 | e20e117c3735 |
--- 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)