From 06ebdec620f8c2daa4a59660b0a9f2bce7eea5de Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Thu, 24 Sep 1998 15:43:19 +0000
Subject: Removed Makefiles from distribution.

---
 doc/Makefile | 13 ++-----------
 1 file changed, 2 insertions(+), 11 deletions(-)

(limited to 'doc/Makefile')

diff --git a/doc/Makefile b/doc/Makefile
index 2799d5ac..bf262c5e 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -15,13 +15,9 @@
 
 DOCNAME = ProofGeneral
 
-# program to make info files from .texi
 MAKEINFO = makeinfo
-# program to make dvi files from .texi
 TEXI2DVI = texi2dvi
-# program to make pdf files from .texi
 TEXI2PDF = texi2pdf
-# program to make html files from .texi
 TEXI2HTML = texi2html 
 
 .SUFFIXES:  .texi .info .dvi .html .pdf
@@ -63,8 +59,8 @@ info:   $(DOCNAME).info
 ## clean: Remove subsidiary documentation files
 ##
 clean:
-	rm -f $(DOCNAME).?? $(DOCNAME).cps $(DOCNAME).cp0
-	rm -f $(DOCNAME).aux $(DOCNAME).log $(DOCNAME).toc
+	rm -f $(DOCNAME).?? $(DOCNAME).fns $(DOCNAME).vrs $(DOCNAME).cps 
+	rm -f $(DOCNAME).aux $(DOCNAME).log $(DOCNAME).toc $(DOCNAME).cp0
 	rm -f *~
 
 ##
@@ -74,11 +70,6 @@ distclean:   clean
 	rm -f $(DOCNAME).info* $(DOCNAME).dvi $(DOCNAME).pdf $(DOCNAME)*.html
 
 
-##
-## cvsclean: remove all non-cvs
-##
-cvsclean: distclean
-
 
 
 
-- 
cgit v1.2.3