diff options
Diffstat (limited to 'etc/refcards/Makefile')
| -rw-r--r-- | etc/refcards/Makefile | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/etc/refcards/Makefile b/etc/refcards/Makefile index 6f8913c5f01..4c5daa9f44c 100644 --- a/etc/refcards/Makefile +++ b/etc/refcards/Makefile @@ -233,10 +233,11 @@ pl-refcard.pdf: $(pl_refcard_deps) fi $(ENVADD) pdftex -output-format=pdf pl-refcard.tex pl-refcard.dvi: $(pl_refcard_deps) - if ! kpsewhich -format=fmt mex > /dev/null; then \ - echo "No mex format found."; false; \ + if kpsewhich -format=fmt mex > /dev/null; then \ + $(ENVADD) tex pl-refcard.tex; \ + else \ + $(ENVADD) mex pl-refcard.tex; \ fi - $(ENVADD) tex pl-refcard.tex pl-refcard.ps: pl-refcard.dvi dvips -t a4 -o $@ pl-refcard.dvi |