diff options
Diffstat (limited to 'Documentation/Makefile')
| -rw-r--r-- | Documentation/Makefile | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/Documentation/Makefile b/Documentation/Makefile index a42320385df3..85f7856f0092 100644 --- a/Documentation/Makefile +++ b/Documentation/Makefile @@ -22,6 +22,8 @@ ifeq ($(HAVE_SPHINX),0) .DEFAULT: $(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 + @./scripts/sphinx-pre-install @echo " SKIP Sphinx $@ target." else # HAVE_SPHINX @@ -95,16 +97,6 @@ endif # HAVE_SPHINX # The following targets are independent of HAVE_SPHINX, and the rules should # work or silently pass without Sphinx. -# no-ops for the Sphinx toolchain -sgmldocs: - @: -psdocs: - @: -mandocs: - @: -installmandocs: - @: - cleandocs: $(Q)rm -rf $(BUILDDIR) $(Q)$(MAKE) BUILDDIR=$(abspath $(BUILDDIR)) $(build)=Documentation/media clean |