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>
Thu, 23 Aug 2018 05:39:00 +0000 (22:39 -0700)
commit10f481831045654d133a34e883ea334524d2e740
tree6774639632775092cb37ca61b956a7d1d89a2668
parent4cc08484df999aa4f8c0d93d77a7ccdb6b0036ea
doc: Don't accidentally create zero-length PDF files

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>
doc/Makefile