etc/options
changeset 56265 785569927666
parent 55672 5e25cc741ab9
child 56279 b4d874f6c6be
     1.1 --- a/etc/options	Sun Mar 23 16:40:35 2014 +0100
     1.2 +++ b/etc/options	Mon Mar 24 12:00:17 2014 +0100
     1.3 @@ -97,6 +97,9 @@
     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  
    1.11  section "Editor Reactivity"
    1.12