Html doc 2
Building the HTML manual generates main00{1,2,3}.png
files for TIKZ figures, which are currently not exported by the manual deployment scripts -- so the manual has missing pictures, see here for example. The present patchset fixes those scripts to include the PNG images, renamed into manual-figure00{1,2,3}.png
.
The fact that the manual is renamed from main.tex
to manual.pdf
makes thing moderately more complex as Hevea generates PNG files whose name is derived from the TEX file. Conceptually the cleanest approach may have been to rename the main00{1,2,3}.png
files into manual-figure00{1,2,3}.png
at deployment time (in the package
rule), but instead I decided to keep the tricky bits in doc/Makefile
and rename there, to keep the deployment scripts simple. (Everything would be simpler if you just renamed main.tex
into manual.tex
, though.)