diff options
| -rw-r--r-- | doc/Makefile.sphinx | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/doc/Makefile.sphinx b/doc/Makefile.sphinx index 933c77ee5..c663c2954 100644 --- a/doc/Makefile.sphinx +++ b/doc/Makefile.sphinx @@ -7,12 +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 +.PHONY: help Makefile.sphinx clean publish + +publish: Makefile.sphinx html singlehtml + 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). |