etc/options
changeset 60845 c4cb46e3cdd1
parent 60843 9980f3bcdea2
child 60884 f3039309702e
--- a/etc/options	Wed Aug 05 16:22:40 2015 +0200
+++ b/etc/options	Wed Aug 05 16:22:56 2015 +0200
@@ -104,7 +104,7 @@
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
-public option ML_debugger_active : bool = false
+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