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?p=pintos-anon;a=commitdiff_plain;h=258ac974c5f71fee4e6e2e10c7b26fda6a823d59;hp=258ac974c5f71fee4e6e2e10c7b26fda6a823d59

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>.
---