etc/options
changeset 62886 72c475e03e22
parent 62875 5a0c06491974
child 63827 b24d0e53dd03
     1.1 --- a/etc/options	Wed Apr 06 11:50:07 2016 +0200
     1.2 +++ b/etc/options	Wed Apr 06 11:57:21 2016 +0200
     1.3 @@ -126,9 +126,6 @@
     1.4  public option ML_system_64 : bool = false
     1.5    -- "ML system for 64bit platform is used if possible (change requires restart)"
     1.6  
     1.7 -option ML_system_bootstrap : bool = false
     1.8 -  -- "provide access to low-level ML system structures (unsafe!)"
     1.9 -
    1.10  
    1.11  section "Editor Reactivity"
    1.12