echo "TeXing documentation" # delete old stuff to avoid spurious or"hidden errors" caused by their presence
rm -f manual.{aux,bbl,blg,dvi,idx,ilg,ind,lab,log,pdf,ps,six,toc}
./buildman.pe -f buildman.config
# TeX the manual
tex manual # ... and build its bibliography
bibtex manual # TeX the manual again to incorporate the ToC
tex manual
tex manual # ... and build the index
../../../doc/manualindex manual # Finally TeX the manual again to get cross-references right
tex manual
# Create PDF version
pdftex manual
pdftex manual
# The HTML version of the manual
mkdir -p ../htm
echo "Creating HTML documentation"
../../../etc/convert.pl -i -u -c -n rds . ../htm
[ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
]
