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