etc/options
changeset 62875 5a0c06491974
parent 62851 07eea2843b82
child 62886 72c475e03e22
--- a/etc/options	Tue Apr 05 18:25:42 2016 +0200
+++ b/etc/options	Tue Apr 05 19:41:58 2016 +0200
@@ -126,8 +126,8 @@
 public option ML_system_64 : bool = false
   -- "ML system for 64bit platform is used if possible (change requires restart)"
 
-option ML_system_unsafe : bool = false
-  -- "provide access to low-level ML system structures"
+option ML_system_bootstrap : bool = false
+  -- "provide access to low-level ML system structures (unsafe!)"
 
 
 section "Editor Reactivity"