From 7a8d87eb57b5c7fa29372c5e4a37f0c40025c0fa Mon Sep 17 00:00:00 2001 From: Chris Hanson Date: Wed, 26 Jul 2000 16:48:19 +0000 Subject: [PATCH] Don't generate .dvi files; do generate .pdf files. --- v7/dist/make-doc-files | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/v7/dist/make-doc-files b/v7/dist/make-doc-files index 785ac7804..42f878539 100755 --- 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 -- 2.25.1