diff --git a/doc/make_doc b/doc/make_doc
index 028b97c..0290847 100755
--- a/doc/make_doc
+++ b/doc/make_doc
@@ -2,15 +2,25 @@
 set -e
 
 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}
+
 # TeX the manual
-pdftex manual
-pdftex manual
+tex manual
+# ... and build its bibliography
+#bibtex manual
+# TeX the manual again to incorporate the ToC
+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
-rm -rf ../htm
-mkdir ../htm
+mkdir -p ../htm
 echo "Creating HTML documentation"
 ../../../etc/convert.pl -i -u -c -n rig . ../htm