doc: Use texi2pdf instead of pdftex.
authorBen Pfaff <blp@cs.stanford.edu>
Tue, 26 Apr 2016 15:32:19 +0000 (08:32 -0700)
committerBen Pfaff <blp@cs.stanford.edu>
Tue, 26 Apr 2016 15:32:19 +0000 (08:32 -0700)
This automatically reruns pdftex if necessary, to make sure that references
are correct.

Reported by David Eck <eck@hws.edu>.


No differences found