diff -r 3d79c132e657 -r 785569927666 etc/options
--- 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"