diff options
Diffstat (limited to 'docs')
-rw-r--r-- | docs/Makefile | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/docs/Makefile b/docs/Makefile index 007a5a9c00..0bf2eb5dff 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -38,7 +38,10 @@ dev-docs: python-dev-docs html: $(DOC_HTML) html/index.html .PHONY: txt -txt: $(DOC_TXT) +txt: + @if which $(POD2TEXT) 1>/dev/null 2>/dev/null; then \ + $(MAKE) $(DOC_TXT); else \ + echo "pod2text not installed; skipping text outputs."; fi .PHONY: python-dev-docs python-dev-docs: |