changeset 73464 | b138cdd22cfb |
parent 73459 | 1f1f4462a6ae |
child 73465 | 1e5c1f8a35cd |
--- a/NEWS Sun Mar 21 23:24:20 2021 +0100 +++ b/NEWS Sun Mar 21 23:56:54 2021 +0100 @@ -877,8 +877,8 @@ *** Document preparation *** -* High-quality blackboard-bold fonts from "txmia" (package "txfonts"), -for A..Z. +* High-quality blackboard-bold symbols from font "txmia" (package +"txfonts"), for A..Z. * Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that are stripped from document output: the effect is to modify the semantic