aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/.cvsignore1
-rw-r--r--kernel/byterun/.cvsignore1
2 files changed, 0 insertions, 2 deletions
diff --git a/kernel/.cvsignore b/kernel/.cvsignore
deleted file mode 100644
index 81f20377e1..0000000000
--- a/kernel/.cvsignore
+++ /dev/null
@@ -1 +0,0 @@
-copcodes.ml
diff --git a/kernel/byterun/.cvsignore b/kernel/byterun/.cvsignore
deleted file mode 100644
index bc5f347b0d..0000000000
--- a/kernel/byterun/.cvsignore
+++ /dev/null
@@ -1 +0,0 @@
-coq_jumptbl.h