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