diff --git a/doc/make_doc b/doc/make_doc
index 39e9ae0..9a9561e 100755
--- a/doc/make_doc
+++ b/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