From 0823923dded755c26f868a6846a89cd0da4d2356 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Mon, 28 Jun 1999 17:42:03 +0000
Subject: Removed accidental deletion of ps file.

---
 doc/Makefile | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'doc/Makefile')

diff --git a/doc/Makefile b/doc/Makefile
index c46965ec..e53fd339 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -75,9 +75,9 @@ ProofGeneral.eps:
 doc:	dvi info
 
 ## 
-## all : build dvi, ps, html, info
+## all : build all documentation targets
 ##
-all:    dvi ps html info
+all:    dvi ps html info 
 
 dvi:    ProofGeneral.eps $(DOCNAME).dvi
 ps:	$(DOCNAME).ps
@@ -94,9 +94,8 @@ info:   ProofGeneral.txt $(DOCNAME).info
 ##
 clean:
 	rm -f ProofGeneral.txt ProofGeneral.eps
-	rm -f $(DOCNAME).?? $(DOCNAME).fns $(DOCNAME).vrs $(DOCNAME).cps 
-	rm -f $(DOCNAME).aux $(DOCNAME).log $(DOCNAME).toc $(DOCNAME).cp0
-	rm -f $(DOCNAME).kys
+	rm -f $(DOCNAME).{cp,fn,vr,tp,ky,pg} 
+	rm -f $(DOCNAME).{fns,vrs,cps,aux,log,toc,kys,cp0}
 	rm -f *~
 
 ##
-- 
cgit v1.2.3