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