etc/options

--- a/etc/options	Wed Apr 15 11:47:29 2015 +0200
+++ b/etc/options	Wed Apr 15 13:55:01 2015 +0200
@@ -101,6 +101,9 @@
 public option ML_exception_trace : bool = false
   -- "ML exception trace for toplevel command execution"
 
+public option ML_statistics : bool = true
+  -- "ML runtime system statistics"
+
 
 section "Editor Reactivity"