diff options
Diffstat (limited to 'systems/doc/pdftex/manual/Makefile')
-rw-r--r-- | systems/doc/pdftex/manual/Makefile | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/systems/doc/pdftex/manual/Makefile b/systems/doc/pdftex/manual/Makefile index 7c1e369ada..05c57fc29a 100644 --- a/systems/doc/pdftex/manual/Makefile +++ b/systems/doc/pdftex/manual/Makefile @@ -1,4 +1,4 @@ -# $Id: Makefile 822 2020-03-02 16:57:37Z karl $ +# $Id: Makefile 848 2021-02-18 17:49:17Z karl $ # Makefile for pdfTeX documentation. Public domain. # Get version we're documenting from the \def in the manual. @@ -52,11 +52,15 @@ pdftex-w.txt: pdftex-w.pdf | expand >$@ || rm -f $@ wc -l pdftex-w.txt # set titlepagelines=half of this -# PDF for the title page. +# PDF for the title page. This should be updated every year; +# - update version numbers +# - make new binary +# - run this target +# Also check pdftex-help.txt for updates. pdftex_binary = ../../source/build-pdftex/texk/web2c/pdftex pdftex-w.pdf: pdftex-w.tex Makefile TEXFONTS=/usr/local/texlive/dev/texmf-dist/fonts// \ - $(pdftex_binary) -ini '\nonstopmode\input $<' + $(pdftex_binary) -ini '$<' # Too annoying to remake help text every time; check by hand when needed. |