--- a/NEWS Tue Mar 25 17:59:34 2014 +0100
+++ b/NEWS Tue Mar 25 19:03:02 2014 +0100
@@ -545,8 +545,13 @@
"ML_exception_trace", which may be also declared within the context via
"declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY.
-* Renamed option "ML_trace" to "ML_source_trace". Minor
-INCOMPATIBILITY.
+* Renamed configuration option "ML_trace" to "ML_source_trace". Minor
+INCOMPATIBILITY.
+
+* Configuration option "ML_print_depth" controls the pretty-printing
+depth of the ML compiler within the context. The old print_depth in
+ML is still available as put_default_print_depth, but rarely used.
+Minor INCOMPATIBILITY.
* Proper context discipline for read_instantiate and instantiate_tac:
variables that are meant to become schematic need to be given as