etc/options
changeset 60889 7f210887cc4e
parent 60884 f3039309702e
child 61158 ea6a4c8bc722
     1.1 --- a/etc/options	Tue Aug 11 13:50:59 2015 +0200
     1.2 +++ b/etc/options	Tue Aug 11 14:13:36 2015 +0200
     1.3 @@ -104,9 +104,6 @@
     1.4  public option ML_debugger : bool = false
     1.5    -- "ML debugger instrumentation for newly compiled code"
     1.6  
     1.7 -public option ML_debugger_active : bool = true
     1.8 -  -- "ML debugger active at run-time, for code compiled with debugger instrumentation"
     1.9 -
    1.10  public option ML_statistics : bool = true
    1.11    -- "ML run-time system statistics"
    1.12