Don't generate .dvi files; do generate .pdf files.

diff --git a/v7/dist/make-doc-files b/v7/dist/make-doc-files
index 785ac7804cfba9d0e117a05352b99e146cd5bf52..42f87853941634256220343a5c72bf06a4f52949 100755 (executable)
--- a/v7/dist/make-doc-files
+++ b/v7/dist/make-doc-files
@@ -9,7 +9,7 @@ mkdir ${prefix}
 mkdir ${tldir}
 
 mans="ref-manual user-manual sos imail"
-types="texinfo info dvi ps html"
+types="texinfo info ps pdf html"
 
 for type in ${types}
 do