diff options
Diffstat (limited to 'contrib/extraction/test')
| -rw-r--r-- | contrib/extraction/test/.cvsignore | 9 |
1 files changed, 0 insertions, 9 deletions
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 |