aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/.cvsignore3
-rw-r--r--dev/doc/.cvsignore1
2 files changed, 0 insertions, 4 deletions
diff --git a/dev/.cvsignore b/dev/.cvsignore
deleted file mode 100644
index 48df473800..0000000000
--- a/dev/.cvsignore
+++ /dev/null
@@ -1,3 +0,0 @@
-other
-ocamldebug-coq
-debug_*
diff --git a/dev/doc/.cvsignore b/dev/doc/.cvsignore
deleted file mode 100644
index 4f4a6839e7..0000000000
--- a/dev/doc/.cvsignore
+++ /dev/null
@@ -1 +0,0 @@
-coq.tex