diff -r 76a8400a58d9 -r 38a64cc17403 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"