From 0641ee042f4f2f0a935877e6be51b3a6fc3135a5 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Tue, 10 Nov 1998 18:15:12 +0000
Subject: added entry to convert dvi into ps.

---
 doc/Makefile | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'doc/Makefile')

diff --git a/doc/Makefile b/doc/Makefile
index e1e11be4..9a2f0cbb 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -19,10 +19,11 @@ DOCNAME = ProofGeneral
 
 MAKEINFO = makeinfo
 TEXI2DVI = texi2dvi
+DVI2PS = dvips
 TEXI2PDF = texi2pdf
 TEXI2HTML = texi2html 
 
-.SUFFIXES:  .texi .info .dvi .html .pdf
+.SUFFIXES:  .texi .info .dvi .html .pdf .ps
 
 .texi.info:
 	$(MAKEINFO) $< 
@@ -30,9 +31,13 @@ TEXI2HTML = texi2html
 .texi.dvi:
 	$(TEXI2DVI) $< 
 
+
 .texi.pdf:
 	$(TEXI2PDF) $< 
 
+.dvi.ps:
+	$(DVI2PS) $< 
+
 .texi.html:	
 	$(TEXI2HTML) $< 
 
-- 
cgit v1.2.3