etc/options
changeset 60884 f3039309702e
parent 60845 c4cb46e3cdd1
child 60889 7f210887cc4e
     1.1 --- a/etc/options	Mon Aug 10 21:06:10 2015 +0200
     1.2 +++ b/etc/options	Mon Aug 10 21:11:15 2015 +0200
     1.3 @@ -107,9 +107,6 @@
     1.4  public option ML_debugger_active : bool = true
     1.5    -- "ML debugger active at run-time, for code compiled with debugger instrumentation"
     1.6  
     1.7 -public option ML_debugger_stepping : bool = false
     1.8 -  -- "ML debugger in single-step mode"
     1.9 -
    1.10  public option ML_statistics : bool = true
    1.11    -- "ML run-time system statistics"
    1.12