diff options
author | Keith Packard <keithp@keithp.com> | 2018-08-22 00:59:59 -0700 |
---|---|---|
committer | Keith Packard <keithp@keithp.com> | 2018-10-02 13:00:32 -0700 |
commit | 8dd942b59edbe6909128b88bfbb8d1e15c3857c6 (patch) | |
tree | ca21bfb570c61f11e110d57753acaefe7a1d6099 /ao-tools | |
parent | 56dcfd4acf830fcb69c8b994e4b989c9aa7ddef3 (diff) |
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>
Diffstat (limited to 'ao-tools')
0 files changed, 0 insertions, 0 deletions