diff options
| -rw-r--r-- | Documentation/Makefile.sphinx | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Documentation/Makefile.sphinx b/Documentation/Makefile.sphinx index 5236f3e2764f..caa8190a3234 100644 --- a/Documentation/Makefile.sphinx +++ b/Documentation/Makefile.sphinx @@ -57,9 +57,10 @@ html: .PHONY: livehtml livehtml: - $(SPHINXAUTOBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR) + @echo "Starting sphinx-autobuild. The HTML pages are in $(BUILDDIR)." + @echo "Press Ctrl-C to stop." @echo - @echo "Autobuild finished. The HTML pages are in $(BUILDDIR)." + $(SPHINXAUTOBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR) .PHONY: dirhtml dirhtml: |