etc/options

--- a/etc/options	Mon Aug 10 21:06:10 2015 +0200
+++ b/etc/options	Mon Aug 10 21:11:15 2015 +0200
@@ -107,9 +107,6 @@
 public option ML_debugger_active : bool = true
   -- "ML debugger active at run-time, for code compiled with debugger instrumentation"
 
-public option ML_debugger_stepping : bool = false
-  -- "ML debugger in single-step mode"
-
 public option ML_statistics : bool = true
   -- "ML run-time system statistics"