etc/options
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"