Tiny texinfo edit.
authorTim Vaughan <tgvaughan@gmail.com>
Sat, 14 Sep 2019 22:24:39 +0000 (00:24 +0200)
committerTim Vaughan <tgvaughan@gmail.com>
Sat, 14 Sep 2019 22:24:39 +0000 (00:24 +0200)

No differences found