diff options
| -rw-r--r-- | Documentation/Makefile.sphinx | 6 |
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 |