diff -r e17f014775a0 -r 09df6a51ad3c etc/options
--- 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"