Revise make_doc

Make it more uniform across all our packages

Author: fingolfin

doc/make_doc

@@ -2,25 +2,20 @@
 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')
+pdftex manual
+# ... and build its bibliography
 bibtex manual
-# TeX the manual again to incorporate the ToC ... and build the index
-tex manual
-tex manual
+# TeX the manual again to incorporate the ToC 
+pdftex 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
 
 # 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 ModIsom . ../htm
-
-#############################################################################
-##
-#E