From: Ben Pfaff <blp@cs.stanford.edu>
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=f67973e1cb1ebb06f155f805c423041fc76ec24a;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 <eck@hws.edu>.
---

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;'