diff options
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/.cvsignore | 1 | ||||
| -rw-r--r-- | contrib/extraction/test/.cvsignore | 9 |
2 files changed, 0 insertions, 10 deletions
diff --git a/contrib/extraction/.cvsignore b/contrib/extraction/.cvsignore deleted file mode 100644 index c446fcb878..0000000000 --- a/contrib/extraction/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -*.v8 diff --git a/contrib/extraction/test/.cvsignore b/contrib/extraction/test/.cvsignore deleted file mode 100644 index 20414aab58..0000000000 --- a/contrib/extraction/test/.cvsignore +++ /dev/null @@ -1,9 +0,0 @@ -theories -ml2v -v2ml -hs2v -v2hs -log -*.hi -*.hs -*.hc |