changeset 56279 | b4d874f6c6be |
parent 56265 | 785569927666 |
child 56613 | 3518ea9f5200 |
--- a/etc/options Tue Mar 25 16:11:00 2014 +0100 +++ b/etc/options Tue Mar 25 16:54:38 2014 +0100 @@ -97,8 +97,11 @@ option process_output_limit : int = 100 -- "build process output limit in million characters (0 = unlimited)" -public option exception_trace : bool = false - -- "exception trace for toplevel command execution" + +section "ML System" + +public option ML_exception_trace : bool = false + -- "ML exception trace for toplevel command execution" section "Editor Reactivity"