--- a/NEWS Wed Sep 11 23:07:18 2024 +0200
+++ b/NEWS Wed Sep 11 23:26:25 2024 +0200
@@ -93,7 +93,8 @@
* Pretty.pure_output_ops and Pretty.pure_string_of support
pretty-printed output without PIDE markup. This is occasionally useful
-for special tools, in contrast to regular user output.
+for special tools, in contrast to regular user output. Manipulation of
+the print_mode via (Print_Mode.setmp []) is no longer required.
* The print_mode "latex" only affects inner syntax variants, while its
impact on Output/Markup/Pretty operations has been removed. Thus the