src/Pure/System/options.ML
changeset 62712 22a17cec2efe
parent 59812 675d0c692c41
child 62791 64ebecf8646c
     1.1 --- a/src/Pure/System/options.ML	Sat Mar 26 12:22:15 2016 +0100
     1.2 +++ b/src/Pure/System/options.ML	Sat Mar 26 12:35:11 2016 +0100
     1.3 @@ -216,6 +216,6 @@
     1.4        end);
     1.5  
     1.6  val _ = load_default ();
     1.7 +val _ = ML_Pretty.print_depth (default_int "ML_print_depth");
     1.8  
     1.9  end;
    1.10 -