aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2005-12-26 14:06:57 +0000
committerherbelin2005-12-26 14:06:57 +0000
commit11edbc28297a9fc782d3117ea3ac7550552609fa (patch)
tree4937152d859a27df4cee7ccebd4b2a4e49c73bd5
parent1061eb505a223ac7cbcec0c5ae9354cd24d9b054 (diff)
Suppression des fichiers .v en ancienne syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7735 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--contrib7/.cvsignore1
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib7/.cvsignore b/contrib7/.cvsignore
deleted file mode 100644
index 7835a7915d..0000000000
--- a/contrib7/.cvsignore
+++ /dev/null
@@ -1 +0,0 @@
-why