etc/options

--- a/etc/options	Tue Jul 30 16:22:07 2013 +0200
+++ b/etc/options	Tue Jul 30 18:19:16 2013 +0200
@@ -123,6 +123,9 @@
 public option editor_chart_delay : real = 3.0
   -- "delay for chart repainting"
 
+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)"