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