NEWS
changeset 56285 9315d3988d73
parent 56281 03c3d1a7c3b8
child 56303 4cc3f4db3447
     1.1 --- a/NEWS	Tue Mar 25 20:12:53 2014 +0100
     1.2 +++ b/NEWS	Wed Mar 26 08:59:53 2014 +0100
     1.3 @@ -550,8 +550,8 @@
     1.4  
     1.5  * Configuration option "ML_print_depth" controls the pretty-printing
     1.6  depth of the ML compiler within the context.  The old print_depth in
     1.7 -ML is still available as put_default_print_depth, but rarely used.
     1.8 -Minor INCOMPATIBILITY.
     1.9 +ML is still available as default_print_depth, but rarely used.  Minor
    1.10 +INCOMPATIBILITY.
    1.11  
    1.12  * Proper context discipline for read_instantiate and instantiate_tac:
    1.13  variables that are meant to become schematic need to be given as