diff options
Diffstat (limited to 'tools/.cvsignore')
| -rw-r--r-- | tools/.cvsignore | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/tools/.cvsignore b/tools/.cvsignore deleted file mode 100644 index 3d7929d7e3..0000000000 --- a/tools/.cvsignore +++ /dev/null @@ -1,7 +0,0 @@ -coqdep_lexer.ml -gallina_lexer.ml -coqdep -coq_makefile -gallina -coq-tex -coqwc.ml |