diff options
Diffstat (limited to 'documentation/Makefile.sphinx')
| -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). |