| changeset 62498 | 5dfcc9697f29 |
| parent 62409 | e391528eff3b |
| child 62711 | 09df6a51ad3c |
--- a/etc/options Wed Mar 02 10:02:12 2016 +0100 +++ b/etc/options Wed Mar 02 19:43:31 2016 +0100 @@ -107,6 +107,9 @@ public option ML_exception_trace : bool = false -- "ML exception trace for toplevel command execution" +public option ML_exception_debugger : bool = false + -- "ML debugger exception trace for toplevel command execution" + public option ML_debugger : bool = false -- "ML debugger instrumentation for newly compiled code"