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 950b0eb59b889d298dde9b4812032ea0172eef08..7f70e4cc34ecb7fa9582c8face73ced4d42ab591 100644 (file)
--- 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)