diff options
Diffstat (limited to 'manual/make.sh')
| -rw-r--r-- | manual/make.sh | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/manual/make.sh b/manual/make.sh new file mode 100644 index 000000000..e8263c7b0 --- /dev/null +++ b/manual/make.sh @@ -0,0 +1,22 @@ +#!/bin/bash + +PDFTEX_OPT="-shell-escape -halt-on-error" + +md5sum *.aux *.bbl *.blg > autoloop.old +set -ex + +pdflatex $PDFTEX_OPT manual.tex +bibtex manual.aux +bibtex weblink.aux + +while + md5sum *.aux *.bbl *.blg > autoloop.new + ! cmp autoloop.old autoloop.new +do + cp autoloop.new autoloop.old + pdflatex $PDFTEX_OPT manual.tex +done + +rm -f autoloop.old +rm -f autoloop.new + |