diff options
Diffstat (limited to 'docs/Makefile')
| -rw-r--r-- | docs/Makefile | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/docs/Makefile b/docs/Makefile index 8806990c96..e9f6c200c3 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -42,7 +42,9 @@ txt: $(DOC_TXT) .PHONY: figs figs: - $(MAKE) -C figs + @set -e ; if which $(FIG2DEV) 1>/dev/null 2>/dev/null; then \ + set -x; $(MAKE) -C figs ; else \ + echo "fig2dev (transfig) not installed; skipping figs."; fi .PHONY: python-dev-docs python-dev-docs: |