etc/options

--- a/etc/options	Tue Aug 11 13:50:59 2015 +0200
+++ b/etc/options	Tue Aug 11 14:13:36 2015 +0200
@@ -104,9 +104,6 @@
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
-public option ML_debugger_active : bool = true
-  -- "ML debugger active at run-time, for code compiled with debugger instrumentation"
-
 public option ML_statistics : bool = true
   -- "ML run-time system statistics"