1 files changed, 10 insertions, 6 deletions

diff --git a/documentation/Makefile.sphinx b/documentation/Makefile.sphinx
index 396998da03..c663c29540 100644
--- a/documentation/Makefile.sphinx
+++ b/documentation/Makefile.sphinx
@@ -7,19 +7,23 @@ SPHINXOPTS    ?=
 SPHINXBUILD   ?= sphinx-build
 SOURCEDIR     = .
 BUILDDIR      = _build
+DESTDIR       = final
 
 # Put it first so that "make" without argument is like "make help".
 help:
         @$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
 
-.PHONY: help Makefile.sphinx publish
+.PHONY: help Makefile.sphinx clean publish
 
 publish: Makefile.sphinx html singlehtml
-        rm -rf $(BUILDDIR)/final/
-        mkdir -p $(BUILDDIR)/final/
-        cp -r $(BUILDDIR)/html/* $(BUILDDIR)/final/
-        cp $(BUILDDIR)/singlehtml/index.html $(BUILDDIR)/final/singleindex.html
-        sed -i -e 's@index.html#@singleindex.html#@g' $(BUILDDIR)/final/singleindex.html
+        rm -rf $(BUILDDIR)/$(DESTDIR)/
+        mkdir -p $(BUILDDIR)/$(DESTDIR)/
+        cp -r $(BUILDDIR)/html/* $(BUILDDIR)/$(DESTDIR)/
+        cp $(BUILDDIR)/singlehtml/index.html $(BUILDDIR)/$(DESTDIR)/singleindex.html
+        sed -i -e 's@index.html#@singleindex.html#@g' $(BUILDDIR)/$(DESTDIR)/singleindex.html
+
+clean:
+        @rm -rf $(BUILDDIR)
 
 # Catch-all target: route all unknown targets to Sphinx using the new
 # "make mode" option.  $(O) is meant as a shortcut for $(SPHINXOPTS).