etc/options
changeset 60765 e43e71a75838
parent 60730 02c2860fcf30
child 60843 9980f3bcdea2
     1.1 --- a/etc/options	Tue Jul 21 14:12:45 2015 +0200
     1.2 +++ b/etc/options	Tue Jul 21 19:04:36 2015 +0200
     1.3 @@ -104,6 +104,12 @@
     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 = false
     1.8 +  -- "ML debugger active at run-time, for code compiled with debugger instrumentation"
     1.9 +
    1.10 +public option ML_debugger_stepping : bool = false
    1.11 +  -- "ML debugger in single-step mode"
    1.12 +
    1.13  public option ML_statistics : bool = true
    1.14    -- "ML runtime system statistics"
    1.15