diff -r e750169a5884 -r cd28423ba19f etc/options
--- a/etc/options	Wed Jul 31 12:31:10 2013 +0200
+++ b/etc/options	Wed Jul 31 12:46:53 2013 +0200
@@ -129,9 +129,6 @@
 option editor_execution_delay : real = 0.02
   -- "delay for start of execution process after document update (seconds)"
 
-option editor_execution_priority : int = -1
-  -- "execution priority of main document structure (e.g. 0, -1, -2)"
-
 
 section "Miscellaneous Tools"