From 258ac974c5f71fee4e6e2e10c7b26fda6a823d59 Mon Sep 17 00:00:00 2001
From: Ben Pfaff <blp@cs.stanford.edu>
Date: Tue, 26 Apr 2016 08:32:19 -0700
Subject: [PATCH] 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>.
---
 doc/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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