equal
deleted
inserted
replaced
105 -- "ML debugger instrumentation for newly compiled code" |
105 -- "ML debugger instrumentation for newly compiled code" |
106 |
106 |
107 public option ML_statistics : bool = true |
107 public option ML_statistics : bool = true |
108 -- "ML run-time system statistics" |
108 -- "ML run-time system statistics" |
109 |
109 |
|
110 public option ML_system_64 : bool = false |
|
111 -- "ML system for 64bit platform is used if possible (change requires restart)" |
|
112 |
110 |
113 |
111 section "Editor Reactivity" |
114 section "Editor Reactivity" |
112 |
115 |
113 public option editor_load_delay : real = 0.5 |
116 public option editor_load_delay : real = 0.5 |
114 -- "delay for file load operations (new buffers etc.)" |
117 -- "delay for file load operations (new buffers etc.)" |