changeset 61158 | ea6a4c8bc722 |
parent 60889 | 7f210887cc4e |
child 61213 | 0b1a092385c7 |
--- a/etc/options Fri Sep 11 17:48:49 2015 +0200 +++ b/etc/options Fri Sep 11 17:57:34 2015 +0200 @@ -107,6 +107,9 @@ public option ML_statistics : bool = true -- "ML run-time system statistics" +public option ML_system_64 : bool = false + -- "ML system for 64bit platform is used if possible (change requires restart)" + section "Editor Reactivity"