diff options
-rw-r--r-- | documentation/Makefile.sphinx | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/documentation/Makefile.sphinx b/documentation/Makefile.sphinx index 933c77ee5f..396998da03 100644 --- a/documentation/Makefile.sphinx +++ b/documentation/Makefile.sphinx | |||
@@ -12,7 +12,14 @@ BUILDDIR = _build | |||
12 | help: | 12 | help: |
13 | @$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) | 13 | @$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) |
14 | 14 | ||
15 | .PHONY: help Makefile.sphinx | 15 | .PHONY: help Makefile.sphinx publish |
16 | |||
17 | publish: Makefile.sphinx html singlehtml | ||
18 | rm -rf $(BUILDDIR)/final/ | ||
19 | mkdir -p $(BUILDDIR)/final/ | ||
20 | cp -r $(BUILDDIR)/html/* $(BUILDDIR)/final/ | ||
21 | cp $(BUILDDIR)/singlehtml/index.html $(BUILDDIR)/final/singleindex.html | ||
22 | sed -i -e 's@index.html#@singleindex.html#@g' $(BUILDDIR)/final/singleindex.html | ||
16 | 23 | ||
17 | # Catch-all target: route all unknown targets to Sphinx using the new | 24 | # Catch-all target: route all unknown targets to Sphinx using the new |
18 | # "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS). | 25 | # "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS). |