aboutsummaryrefslogtreecommitdiff
path: root/Makefile.doc
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.doc')
-rw-r--r--Makefile.doc3
1 files changed, 3 insertions, 0 deletions
diff --git a/Makefile.doc b/Makefile.doc
index effd624cff..8be032ceb3 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -100,6 +100,9 @@ doc-stdlib: \
full-stdlib: \
doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.pdf
+sphinx-clean:
+ rm -rf $(SPHINXBUILDDIR)
+
.PHONY: plugin-tutorial
plugin-tutorial: states tools
+$(MAKE) COQBIN=$(PWD)/bin/ -C $(PLUGINTUTO)