diff -r c1521c003e78 -r 2e3e2ec20e87 NEWS --- a/NEWS Mon Sep 09 21:54:41 2024 +0200 +++ b/NEWS Mon Sep 09 22:04:46 2024 +0200 @@ -83,6 +83,15 @@ purposes. +*** ML *** + +* Constructors for type Pretty.T (such as Pretty.str, Pretty.mark_str, +Pretty.markup_block) are now value-oriented. Use of the global +print_mode is restricted to ultimate Pretty.string_of (and some +variants), while the underlying Pretty.output operation supports an +explicit Pretty.output_ops argument for alternative applications. + + *** System *** * The Build_Manager module has replaced previous glue-code for Jenkins