diff options
Diffstat (limited to 'distrib/.cvsignore')
| -rw-r--r-- | distrib/.cvsignore | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/distrib/.cvsignore b/distrib/.cvsignore deleted file mode 100644 index 46e8aed30..000000000 --- a/distrib/.cvsignore +++ /dev/null @@ -1,17 +0,0 @@ -rpmbuildroot -i386 -tar-i386 -sun4 -alpha -apx -alpha -ppc -redhat -config.distrib -coq-* -contrib-* -patch-* -deb_build -coq_* -sun4u -*.rpm |