diff options
Diffstat (limited to 'Master/texmf-dist/doc/pdftex/manual/Makefile')
-rw-r--r-- | Master/texmf-dist/doc/pdftex/manual/Makefile | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Master/texmf-dist/doc/pdftex/manual/Makefile b/Master/texmf-dist/doc/pdftex/manual/Makefile index 001768d614b..102d82ff576 100644 --- a/Master/texmf-dist/doc/pdftex/manual/Makefile +++ b/Master/texmf-dist/doc/pdftex/manual/Makefile @@ -1,4 +1,4 @@ -# $Id: Makefile 745 2016-04-25 18:06:57Z karl $ +# $Id: Makefile 751 2016-05-04 22:57:38Z karl $ # Makefile for pdfTeX documentation. Public domain. # Get version we're documenting from the \def in the manual. @@ -58,8 +58,9 @@ pdftex-w.pdf: pdftex-w.tex # Too annoying to remake help text every time; check by hand when needed. -pdftex-help.txt: +pdftex-help.txt: force $(pdftex_binary) --help >$@ || rm -f $@ +force: # if we don't have a build tree around, just try from the path. build_binary := ../../source/build-pdftex/texk/web2c/pdftex |