changeset 52773 | 3e8b9d2f18cb |
parent 52759 | a20631db9c8a |
child 52779 | 82707f95a783 |
--- a/etc/options Mon Jul 29 15:59:47 2013 +0200 +++ b/etc/options Mon Jul 29 16:01:05 2013 +0200 @@ -123,7 +123,7 @@ public option editor_chart_delay : real = 3.0 -- "delay for chart repainting" -public option editor_execution_priority : int = -2 +option editor_execution_priority : int = -1 -- "execution priority of main document structure (e.g. 0, -1, -2)" option editor_execution_range : string = "visible"