aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1998-10-07 16:02:34 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1998-10-07 16:02:34 +0000
commit861e84ded233af103dbd7ddbb7fa597f9efac610 (patch)
tree44ae20c4aaa2f18340defb00b66b24703583a313
parent666f11805d750e246a6ccf1dd54fff607443314b (diff)
Added cvsclean back
-rw-r--r--Makefile.devel12
1 files changed, 11 insertions, 1 deletions
diff --git a/Makefile.devel b/Makefile.devel
index 56aa2b3a..a6b7fee4 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -49,7 +49,7 @@ EMACS=xemacs
# Files not to include the distribution area or tarball
-NONDISTFILES=todo html etc Makefile doc/Makefile images/*.xcf images/notes.txt
+NONDISTFILES=todo html etc Makefile doc/Makefile images/*.xcf images/notes.txt images/gimp
# Files not to include in the distribution tarball
IGNOREDFILES=doc/ProofGeneral.dvi
@@ -96,6 +96,7 @@ ChangeLog: FORCE
#
clean:
(cd doc; $(MAKE) clean)
+ (cd images; $(MAKE) clean)
############################################################
@@ -103,8 +104,17 @@ clean:
# Clean up all generated files.
#
distclean: clean
+ (cd doc; $(MAKE) distclean)
+ (cd images; $(MAKE) distclean)
+
+############################################################
+#
+# Clean up all non-cvs files.
+#
+cvsclean: clean
rm -rf $(FILES_NONCVS)
(cd doc; $(MAKE) distclean)
+ (cd images; $(MAKE) cvsclean)
############################################################
#