etc/options
changeset 62875 5a0c06491974
parent 62851 07eea2843b82
child 62886 72c475e03e22
equal deleted inserted replaced
62874:b0194643e64c 62875:5a0c06491974
   124   -- "ML run-time system statistics"
   124   -- "ML run-time system statistics"
   125 
   125 
   126 public option ML_system_64 : bool = false
   126 public option ML_system_64 : bool = false
   127   -- "ML system for 64bit platform is used if possible (change requires restart)"
   127   -- "ML system for 64bit platform is used if possible (change requires restart)"
   128 
   128 
   129 option ML_system_unsafe : bool = false
   129 option ML_system_bootstrap : bool = false
   130   -- "provide access to low-level ML system structures"
   130   -- "provide access to low-level ML system structures (unsafe!)"
   131 
   131 
   132 
   132 
   133 section "Editor Reactivity"
   133 section "Editor Reactivity"
   134 
   134 
   135 public option editor_load_delay : real = 0.5
   135 public option editor_load_delay : real = 0.5