aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1998-12-17 17:58:15 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1998-12-17 17:58:15 +0000
commit4d0b70c4adfc233462afd66770c39a2fedccb5e0 (patch)
tree12a17af29b298b5709e299e8fe661acd57c9e51d
parenta1de8b2ccae29c365560b8a3be3309fa6506d57d (diff)
Removed .cvsignore files from distribution.
-rw-r--r--Makefile.devel2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.devel b/Makefile.devel
index d19dfd96..53c5c444 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -88,7 +88,7 @@ TAR=tar
DEVELMAKE=make -f Makefile.devel
# Files not to include the distribution area or tarball
-NONDISTFILES=html etc Makefile.devel doc/notes.txt images/*.xcf images/notes.txt images/gimp images/Makefile isa/wip.ML
+NONDISTFILES=.cvsignore */.cvsignore html etc Makefile.devel doc/notes.txt images/*.xcf images/notes.txt images/gimp images/Makefile isa/wip.ML
# Files not to include in the distribution tarball
IGNOREDFILES=doc/ProofGeneral.dvi Makefile.devel todo isa/wip.ML