diff options
Diffstat (limited to 'docs/Makefile.sphinx')
| -rw-r--r-- | docs/Makefile.sphinx | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/docs/Makefile.sphinx b/docs/Makefile.sphinx index 21f66488b2..81c13de9cd 100644 --- a/docs/Makefile.sphinx +++ b/docs/Makefile.sphinx @@ -46,6 +46,10 @@ clean: html: $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html @echo + @# FIXME: Remove this `cp` once HTML->Sphinx transition is completed. + @# Kind of a hack, but HTML-formatted docs are on the way out anyway. + @echo "Copying legacy HTML-formatted docs into $(BUILDDIR)/html" + @cp -a *.html tutorial $(BUILDDIR)/html @echo "Build finished. The HTML pages are in $(BUILDDIR)/html." dirhtml: |