X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pintos-anon;a=blobdiff_plain;f=doc%2FMakefile;fp=doc%2FMakefile;h=95dd71bdf0e6c5a0dfed6a06f0c6bdd60228df2a;hp=0a01cc3ac8a26e27d0e94b895409716adb73d3dc;hb=258ac974c5f71fee4e6e2e10c7b26fda6a823d59;hpb=8b39127d9437709ab55ad1ed7ac4fb65245fc57b

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