htmldoc has been installed, but it’s a hacky solution to the problem that doesn’t really work at the moment (particularly bad utf-8 support as well). I’m going to stop trying to force it to work.
The mediawiki team are actually re-working PDF rendering for the
Book stuff: https://www.mediawiki.org/wiki/Reading/Web/PDF_Functionality and still haven’t gotten it running. When they do I’m sure we’ll pick it up as part of updating our install.
In the meantime, I’ll look at a way of generating a static PDF from the book manually (on a cron job probably), and link/upload it to the site.
For now, if you want stuff as a PDF, I recommend using your browser to print, and particularly
Save as PDF if it’s available (Chrome/Chromium should have this by default).
The actual pages the book is composed of can be found here:
You can walk through that list and print each section as needed. As soon as we get a static PDF of that book printed I’ll link to it from here.