`make doc-pdf`: Reduce output

Building the PDF documentation creates an excessive amount of log output: half a million lines, 55 MB. In particular in the GH Actions CI it is impractical to view the log in the browser, even as a raw log.

We should silence the pdflatex runs so that only errors are displayed.
