Commit 2cedbfeb authored by Gabriel Scherer's avatar Gabriel Scherer

HTML manual: change the naming of Hevea-generated image files

parent 70328180
......@@ -16,13 +16,22 @@ all: main.pdf main.html
main.html: main.tex $(DEPS) $(wildcard *.hva)
hevea -fix main.tex
@# Hevea interprets 'tabbing' environment in a way
@# that creates spacing errors in the rendered output
@# of "textual version of derivation trees": it
@# asks for (padding:0px;) while the TeX rendering
@# inserts spacing between columns. Change this
@# to {padding:1px;}
#
# Hevea interprets 'tabbing' environment in a way
# that creates spacing errors in the rendered output
# of "textual version of derivation trees": it
# asks for (padding:0px;) while the TeX rendering
# inserts spacing between columns. Change this
# to {padding:1px;}
$(SED) -i -e "s/cellpadding0/cellpadding1/" main.html
#
# Hevea generates images main00{1,2,3}.png for the tikz pictures
# present in the manual. Rename them into manual-figure00{1,2,3}.png
# for consistency with the naming scheme of the deployed manual files.
for f in 1 2 3; do \
mv main00$$f.png manual-figure00$$f.png; \
done
$(SED) --in-place 's/<img src="main/<img src="manual-figure/g' main.html
loop:
latexmk -pdf -pvc main
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment