doc: Don't accidentally create zero-length PDF files
authorKeith Packard <keithp@keithp.com>
Wed, 22 Aug 2018 07:59:59 +0000 (00:59 -0700)
committerKeith Packard <keithp@keithp.com>
Tue, 2 Oct 2018 20:00:32 +0000 (13:00 -0700)
The PDF files are generated at the same time the HTML files are, so
the PDF versions depend on the HTML ones. However, touching the PDF
files is a bad idea.

Signed-off-by: Keith Packard <keithp@keithp.com>

No differences found