src/Pure/ex/document/root.tex
Tue, 23 Nov 2021 21:02:13 +0100 wenzelm example: alternative document headings, based on more general document output markup;
less more (0) tip