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