diff --git a/doc/make_doc b/doc/make_doc index 19c3f06..9b3ac74 100755 --- a/doc/make_doc +++ b/doc/make_doc @@ -2,25 +2,25 @@ set -e echo "TeXing documentation" +# delete old stuff to avoid spurious or "hidden errors" caused by their presence +rm -f manual.aux manual.pdf manual.idx manual.ilg manual.ind manual.lab manual.log manual.six manual.toc # TeX the manual tex manual -# ... and build its bibliography (uncomment if there is a `manual.bib') +# ... and build its bibliography bibtex manual -# TeX the manual again to incorporate the ToC ... and build the index +# 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 +pdftex manual +pdftex manual # The HTML version of the manual -rm -rf ../htm -mkdir ../htm +mkdir -p ../htm echo "Creating HTML documentation" ../../../etc/convert.pl -i -u -c -n ActionTestOldDocPackage . ../htm - -############################################################################# -## -#E