changeset 52715 | 8979d830950b |
parent 52714 | a4e4802753b9 |
child 52746 | eec610972763 |
--- a/etc/options Sat Jul 20 16:18:17 2013 +0200 +++ b/etc/options Sat Jul 20 16:27:55 2013 +0200 @@ -123,6 +123,9 @@ public option editor_chart_delay : real = 3.0 -- "delay for chart repainting" +public option editor_execution_priority : int = -2 + -- "execution priority of main document structure (e.g. 0, -1, -2)" + section "Miscellaneous Tools"