# HG changeset patch
# User wenzelm
# Date 1597224361 -7200
# Node ID 98dca728fc9c24a3ce629276db774160bec48dc2
# Parent  f67e83608745e46c6e7c04ad272f3b9336239413
removed pointless option "ML_statistics": always enabled;

diff -r f67e83608745 -r 98dca728fc9c etc/options
--- a/etc/options	Wed Aug 12 11:22:11 2020 +0200
+++ b/etc/options	Wed Aug 12 11:26:01 2020 +0200
@@ -138,9 +138,6 @@
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
-public option ML_statistics : bool = true
-  -- "ML run-time system statistics"
-
 public option ML_system_64 : bool = false
   -- "ML system for 64bit platform is used if possible (change requires restart)"
 
diff -r f67e83608745 -r 98dca728fc9c src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed Aug 12 11:22:11 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Wed Aug 12 11:26:01 2020 +0200
@@ -74,7 +74,7 @@
 
     private def consume(props: Properties.T): Unit = synchronized
     {
-      if (session != null && session.session_options.bool("ML_statistics")) {
+      if (session != null) {
         val stats = Session.Runtime_Statistics(session.xml_cache.props(props))
         session.runtime_statistics.post(stats)
       }
diff -r f67e83608745 -r 98dca728fc9c src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Aug 12 11:22:11 2020 +0200
+++ b/src/Pure/Tools/build.scala	Wed Aug 12 11:26:01 2020 +0200
@@ -493,7 +493,6 @@
   {
     val build_options =
       options +
-        "ML_statistics" +
         "completion_limit=0" +
         "editor_tracing_messages=0" +
         "pide_reports=false"
diff -r f67e83608745 -r 98dca728fc9c src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Wed Aug 12 11:22:11 2020 +0200
+++ b/src/Pure/Tools/dump.scala	Wed Aug 12 11:26:01 2020 +0200
@@ -106,7 +106,6 @@
         val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
         val options1 =
           options0 +
-            "ML_statistics=false" +
             "parallel_proofs=0" +
             "completion_limit=0" +
             "editor_tracing_messages=0" +