| changeset 81117 | 0c898f7d9b15 |
| parent 81116 | 0fb1e2dd4122 |
| child 81121 | 7cacedbddba7 |
--- a/NEWS Sat Oct 05 14:58:36 2024 +0200 +++ b/NEWS Sat Oct 05 15:18:49 2024 +0200 @@ -139,6 +139,8 @@ Note that basic Markup.markup cannot be used for Latex output: proper Pretty.T operations are required (e.g. Pretty.mark_str). +* Antiquotation \<^bundle>\<open>name\<close> inlines a formally checked bundle name. + *** System ***