etc/options
changeset 52715 8979d830950b
parent 52714 a4e4802753b9
child 52746 eec610972763
     1.1 --- a/etc/options	Sat Jul 20 16:18:17 2013 +0200
     1.2 +++ b/etc/options	Sat Jul 20 16:27:55 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 +public option editor_execution_priority : int = -2
     1.8 +  -- "execution priority of main document structure (e.g. 0, -1, -2)"
     1.9 +
    1.10  
    1.11  section "Miscellaneous Tools"
    1.12