equal
deleted
inserted
replaced
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 |