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)"