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)
commit8dd942b59edbe6909128b88bfbb8d1e15c3857c6
treeca21bfb570c61f11e110d57753acaefe7a1d6099
parent56dcfd4acf830fcb69c8b994e4b989c9aa7ddef3
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