equal
deleted
inserted
replaced
105 section "ML System" |
105 section "ML System" |
106 |
106 |
107 public option ML_exception_trace : bool = false |
107 public option ML_exception_trace : bool = false |
108 -- "ML exception trace for toplevel command execution" |
108 -- "ML exception trace for toplevel command execution" |
109 |
109 |
|
110 public option ML_exception_debugger : bool = false |
|
111 -- "ML debugger exception trace for toplevel command execution" |
|
112 |
110 public option ML_debugger : bool = false |
113 public option ML_debugger : bool = false |
111 -- "ML debugger instrumentation for newly compiled code" |
114 -- "ML debugger instrumentation for newly compiled code" |
112 |
115 |
113 public option ML_statistics : bool = true |
116 public option ML_statistics : bool = true |
114 -- "ML run-time system statistics" |
117 -- "ML run-time system statistics" |