etc/options
changeset 52759 a20631db9c8a
parent 52746 eec610972763
child 52773 3e8b9d2f18cb
     1.1 --- a/etc/options	Sun Jul 28 20:51:15 2013 +0200
     1.2 +++ b/etc/options	Mon Jul 29 12:50:16 2013 +0200
     1.3 @@ -126,6 +126,9 @@
     1.4  public option editor_execution_priority : int = -2
     1.5    -- "execution priority of main document structure (e.g. 0, -1, -2)"
     1.6  
     1.7 +option editor_execution_range : string = "visible"
     1.8 +  -- "range of continuous document processing: all, none, visible"
     1.9 +
    1.10  
    1.11  section "Miscellaneous Tools"
    1.12