On 17 January 2017 at 14:23, Markus Armbruster <arm...@redhat.com> wrote: > Peter Maydell <peter.mayd...@linaro.org> writes: >> As an aside, how useful is the PDF output anyway? In 2017 >> there seems to me quite a good argument for just creating >> HTML... > > We do generate HTML. We also generate PDF. It's better for printing > (if you're so inclined), and it costs us next to nothing: a couple of > lines in the top-level Makefile.
Mmm, but in thinking about other possible document formats it would be interesting to know whether not producing PDF would be a dealbreaker or just dropping a feature that three people use... In any case, applied this pullreq to master. Interestingly there were no signs of the "unlikely character" warnings this time around. thanks -- PMM
