From: Ben Pfaff Date: Tue, 26 Apr 2016 15:32:19 +0000 (-0700) Subject: doc: Use texi2pdf instead of pdftex. X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=258ac974c5f71fee4e6e2e10c7b26fda6a823d59;p=pintos-anon doc: Use texi2pdf instead of pdftex. This automatically reruns pdftex if necessary, to make sure that references are correct. Reported by David Eck . --- diff --git a/doc/Makefile b/doc/Makefile index 0a01cc3..95dd71b 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -21,7 +21,7 @@ pintos.ps: pintos.dvi dvips $< -o $@ pintos.pdf: $(TEXIS) - pdftex $< -o $@ + texi2pdf $< -o $@ %.texi: % sed < $< > $@ 's/\([{}@]\)/\@\1/g;'