etc/options
changeset 52779 82707f95a783
parent 52773 3e8b9d2f18cb
child 52798 9d3c9862d1dd
     1.1 --- a/etc/options	Mon Jul 29 20:38:40 2013 +0200
     1.2 +++ b/etc/options	Mon Jul 29 20:46:21 2013 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4    -- "execution priority of main document structure (e.g. 0, -1, -2)"
     1.5  
     1.6  option editor_execution_range : string = "visible"
     1.7 -  -- "range of continuous document processing: all, none, visible"
     1.8 +  -- "execution range of continuous document processing: all, none, visible"
     1.9  
    1.10  
    1.11  section "Miscellaneous Tools"