Is anyone strongly against stopping the generation of pdf docs?

CI is currently broken because of a LaTeX error. It happens every now and then, and it blocks other PRs. LaTeX error messages being what they are, these issues can take time and effot to fix.

Should we just stop generating the pdfs? It makes us waste time, and I personally doubt these are really useful anyway. We could just provide an archive of the html docs instead, which would be more readable.