etc/options
changeset 52798 9d3c9862d1dd
parent 52779 82707f95a783
child 52807 b859a180936b
     1.1 --- a/etc/options	Tue Jul 30 16:22:07 2013 +0200
     1.2 +++ b/etc/options	Tue Jul 30 18:19:16 2013 +0200
     1.3 @@ -123,6 +123,9 @@
     1.4  public option editor_chart_delay : real = 3.0
     1.5    -- "delay for chart repainting"
     1.6  
     1.7 +option editor_execution_delay : real = 0.02
     1.8 +  -- "delay for start of execution process after document update (seconds)"
     1.9 +
    1.10  option editor_execution_priority : int = -1
    1.11    -- "execution priority of main document structure (e.g. 0, -1, -2)"
    1.12