etc/options
changeset 62498 5dfcc9697f29
parent 62409 e391528eff3b
child 62711 09df6a51ad3c
     1.1 --- a/etc/options	Wed Mar 02 10:02:12 2016 +0100
     1.2 +++ b/etc/options	Wed Mar 02 19:43:31 2016 +0100
     1.3 @@ -107,6 +107,9 @@
     1.4  public option ML_exception_trace : bool = false
     1.5    -- "ML exception trace for toplevel command execution"
     1.6  
     1.7 +public option ML_exception_debugger : bool = false
     1.8 +  -- "ML debugger exception trace for toplevel command execution"
     1.9 +
    1.10  public option ML_debugger : bool = false
    1.11    -- "ML debugger instrumentation for newly compiled code"
    1.12