diff --git a/docs/Makefile b/docs/Makefile
index 3a9d3de8..cef2e832 100644
--- a/docs/Makefile
+++ b/docs/Makefile
@@ -12,25 +12,23 @@ ALLSPHINXOPTS   = -d $(BUILDDIR)/doctrees $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) sou
 GH_PAGES_SOURCES = source Makefile
 GH_SOURCE_BRANCH = develop
 
-.PHONY: clean html gh-pages
+.PHONY: html clean html latexpdf
+
+help:
+	@echo "Please use \`make <target>' where <target> is one of"
+	@echo "  html       to make standalone HTML files"
+	@echo "  latexpdf   to make LaTeX files and run them through pdflatex"
 
 clean:
 	-rm -rf $(BUILDDIR)/*
 
+latexpdf:
+	$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
+	@echo "Running LaTeX files through pdflatex..."
+	$(MAKE) -C $(BUILDDIR)/latex all-pdf
+	@echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
+
 html:
 	$(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html
 	@echo
 	@echo "Build finished. The HTML pages are in $(BUILDDIR)/html."
-
-gh-pages:
-	git checkout gh-pages
-	find .. -maxdepth 1 ! -name '.git*' -and ! -name 'docs' -exec rm -rf {} \;
-	git checkout ${GH_SOURCE_BRANCH} ${GH_PAGES_SOURCES}
-	git reset HEAD
-	make html
-	mv -fv _build/html/* ..
-	rm -rf _build ${GH_PAGES_SOURCES}
-	git add ..
-	git commit -m "Create gh-pages for '`git log develop -1 --pretty=oneline --abbrev-commit`'"
-	git push origin gh-pages
-	git checkout ${GH_SOURCE_BRANCH}