diff --git a/docs/Makefile b/docs/Makefile index 61a0dd90d3c5750ab7e3465a27475ff5c9c2dc67..bb6819d4f6c6b94c3949a8b86d38e102f4658880 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -51,6 +51,9 @@ html: @echo @echo "Build finished. The HTML pages are in $(BUILDDIR)/html." +watch_html: + while :; do inotifywait -e modify -e create -e delete -e move -r .. && make html; done + dirhtml: $(SPHINXBUILD) -b dirhtml $(ALLSPHINXOPTS) $(BUILDDIR)/dirhtml @echo