etc/options
changeset 52810 cd28423ba19f
parent 52807 b859a180936b
child 53189 ee8b8dafef0e
     1.1 --- a/etc/options	Wed Jul 31 12:31:10 2013 +0200
     1.2 +++ b/etc/options	Wed Jul 31 12:46:53 2013 +0200
     1.3 @@ -129,9 +129,6 @@
     1.4  option editor_execution_delay : real = 0.02
     1.5    -- "delay for start of execution process after document update (seconds)"
     1.6  
     1.7 -option editor_execution_priority : int = -1
     1.8 -  -- "execution priority of main document structure (e.g. 0, -1, -2)"
     1.9 -
    1.10  
    1.11  section "Miscellaneous Tools"
    1.12