manual/generate: Always generate a PDF manual as well by default.
authorUwe Hermann <uwe@hermann-uwe.de>
Thu, 6 Sep 2018 07:50:57 +0000 (09:50 +0200)
committerUwe Hermann <uwe@hermann-uwe.de>
Thu, 6 Sep 2018 12:52:10 +0000 (14:52 +0200)

No differences found