diff -r b610ba36e02c -r e43e71a75838 etc/options
--- a/etc/options	Tue Jul 21 14:12:45 2015 +0200
+++ b/etc/options	Tue Jul 21 19:04:36 2015 +0200
@@ -104,6 +104,12 @@
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
+public option ML_debugger_active : bool = false
+  -- "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 runtime system statistics"