From: Taylor R Campbell <campbell@mumble.net>
Date: Fri, 30 Aug 2013 15:45:21 +0000 (+0000)
Subject: Use `texi2dvi --pdf', not `texi2pdf'.
X-Git-Tag: release-9.2.0~140
X-Git-Url: https://birchwood-abbey.net/git?a=commitdiff_plain;h=2c9f3184f959a1eed7363252d486efe2140b9a4e;p=mit-scheme.git

Use `texi2dvi --pdf', not `texi2pdf'.

No functional difference, but texi2pdf is a newer utility not found
in older versions of GNU Texinfo that are still prevalent.
---

diff --git a/doc/make-common.in b/doc/make-common.in
index 950b0eb59..7f70e4cc3 100644
--- a/doc/make-common.in
+++ b/doc/make-common.in
@@ -81,7 +81,7 @@ $(HTML_TARGET)/index.html: $(SOURCES)
 	makeinfo --html $(TEXINFO_ROOT).texinfo
 
 $(PDF_TARGET): $(SOURCES)
-	texi2pdf $(TEX_OPTIONS) --output=$@ $(TEXINFO_ROOT).texinfo
+	texi2dvi --pdf $(TEX_OPTIONS) --output=$@ $(TEXINFO_ROOT).texinfo
 
 $(PS_TARGET): $(SOURCES)
 	-rm -f $(DVI_TARGET)