diff options
Diffstat (limited to 'docs/Makefile')
-rw-r--r-- | docs/Makefile | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/docs/Makefile b/docs/Makefile index 9756fab286..d81d11eeb2 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -6,6 +6,9 @@ SPHINXOPTS = SPHINXBUILD = sphinx-build PAPER = BUILDDIR = build/$(MICROPY_PORT) +# Run "make FORCE= ..." to avoid rebuilding from scratch (and risk +# producing incorrect docs). +FORCE = -E # User-friendly check for sphinx-build ifeq ($(shell which $(SPHINXBUILD) >/dev/null 2>&1; echo $$?), 1) @@ -50,7 +53,7 @@ clean: rm -rf $(BUILDDIR)/* html: - $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html + $(SPHINXBUILD) $(FORCE) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html @echo @echo "Build finished. The HTML pages are in $(BUILDDIR)/html." @@ -111,7 +114,7 @@ latex: "(use \`make latexpdf' here to do that automatically)." latexpdf: - $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex + $(SPHINXBUILD) $(FORCE) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex @echo "Running LaTeX files through pdflatex..." $(MAKE) -C $(BUILDDIR)/latex all-pdf @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex." |