etc/options
changeset 56279 b4d874f6c6be
parent 56265 785569927666
child 56613 3518ea9f5200
     1.1 --- a/etc/options	Tue Mar 25 16:11:00 2014 +0100
     1.2 +++ b/etc/options	Tue Mar 25 16:54:38 2014 +0100
     1.3 @@ -97,8 +97,11 @@
     1.4  option process_output_limit : int = 100
     1.5    -- "build process output limit in million characters (0 = unlimited)"
     1.6  
     1.7 -public option exception_trace : bool = false
     1.8 -  -- "exception trace for toplevel command execution"
     1.9 +
    1.10 +section "ML System"
    1.11 +
    1.12 +public option ML_exception_trace : bool = false
    1.13 +  -- "ML exception trace for toplevel command execution"
    1.14  
    1.15  
    1.16  section "Editor Reactivity"