etc/options
changeset 52773 3e8b9d2f18cb
parent 52759 a20631db9c8a
child 52779 82707f95a783
     1.1 --- a/etc/options	Mon Jul 29 15:59:47 2013 +0200
     1.2 +++ b/etc/options	Mon Jul 29 16:01:05 2013 +0200
     1.3 @@ -123,7 +123,7 @@
     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 +option editor_execution_priority : int = -1
     1.9    -- "execution priority of main document structure (e.g. 0, -1, -2)"
    1.10  
    1.11  option editor_execution_range : string = "visible"