equal
deleted
inserted
replaced
99 section "ML System" |
99 section "ML System" |
100 |
100 |
101 public option ML_exception_trace : bool = false |
101 public option ML_exception_trace : bool = false |
102 -- "ML exception trace for toplevel command execution" |
102 -- "ML exception trace for toplevel command execution" |
103 |
103 |
|
104 public option ML_debugger : bool = false |
|
105 -- "ML debugger instrumentation for newly compiled code" |
|
106 |
104 public option ML_statistics : bool = true |
107 public option ML_statistics : bool = true |
105 -- "ML runtime system statistics" |
108 -- "ML runtime system statistics" |
106 |
109 |
107 |
110 |
108 section "Editor Reactivity" |
111 section "Editor Reactivity" |