changeset 62711 | 09df6a51ad3c |
parent 62498 | 5dfcc9697f29 |
child 62790 | 0c526d2fb609 |
--- a/etc/options Sat Mar 26 12:17:02 2016 +0100 +++ b/etc/options Sat Mar 26 12:22:15 2016 +0100 @@ -104,6 +104,9 @@ section "ML System" +option ML_print_depth : int = 20 + -- "ML print depth for toplevel pretty-printing" + public option ML_exception_trace : bool = false -- "ML exception trace for toplevel command execution"