summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--Documentation/Makefile.sphinx6
1 files changed, 6 insertions, 0 deletions
diff --git a/Documentation/Makefile.sphinx b/Documentation/Makefile.sphinx
index 6c203745b6c6..d8d13c92a178 100644
--- a/Documentation/Makefile.sphinx
+++ b/Documentation/Makefile.sphinx
@@ -17,6 +17,12 @@ ifeq ($(HAVE_SPHINX),0)
$(warning The '$(SPHINXBUILD)' command was not found. Make sure you have Sphinx installed and in PATH, or set the SPHINXBUILD make variable to point to the full path of the '$(SPHINXBUILD)' executable.)
@echo " SKIP Sphinx $@ target."
+else ifneq ($(DOCBOOKS),)
+
+# Skip Sphinx build if the user explicitly requested DOCBOOKS.
+.DEFAULT:
+ @echo " SKIP Sphinx $@ target (DOCBOOKS specified)."
+
else # HAVE_SPHINX
# User-friendly check for rst2pdf