etc/options

--- a/etc/options	Sat Jul 20 16:18:17 2013 +0200
+++ b/etc/options	Sat Jul 20 16:27:55 2013 +0200
@@ -123,6 +123,9 @@
 public option editor_chart_delay : real = 3.0
   -- "delay for chart repainting"
 
+public option editor_execution_priority : int = -2
+  -- "execution priority of main document structure (e.g. 0, -1, -2)"
+
 
 section "Miscellaneous Tools"