chiark / gitweb /
common/defs.man: Set the font for the running headers as well as the body.
authorMark Wooding <mdw@distorted.org.uk>
Mon, 20 Sep 2021 14:05:48 +0000 (15:05 +0100)
committerMark Wooding <mdw@distorted.org.uk>
Mon, 20 Sep 2021 14:05:48 +0000 (15:05 +0100)
This involves switching environments.


No differences found