diff -r 000000000000 -r 2b3e5ec03512 doc/manual/latex/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/manual/latex/Makefile	Thu Apr 21 14:57:45 2011 +0100
@@ -0,0 +1,19 @@
+all: clean refman.pdf
+
+pdf: refman.pdf
+
+refman.pdf: refman.tex
+	pdflatex refman.tex
+	makeindex refman.idx
+	pdflatex refman.tex
+	latex_count=5 ; \
+	while egrep -s 'Rerun (LaTeX|to get cross-references right)' refman.log && [ $$latex_count -gt 0 ] ;\
+	    do \
+	      echo "Rerunning latex...." ;\
+	      pdflatex refman.tex ;\
+	      latex_count=`expr $$latex_count - 1` ;\
+	    done
+
+
+clean:
+	rm -f *.ps *.dvi *.aux *.toc *.idx *.ind *.ilg *.log *.out refman.pdf