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