Mentions légales du service

Skip to content

Html doc 2

SCHERER Gabriel requested to merge gscherer/menhir:html-doc-2 into master

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.)

Merge request reports