diff options
Diffstat (limited to 'bin')
| -rw-r--r-- | bin/.cvsignore | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/bin/.cvsignore b/bin/.cvsignore deleted file mode 100644 index 8a0fce7d0b..0000000000 --- a/bin/.cvsignore +++ /dev/null @@ -1,21 +0,0 @@ -coqc -coqmktop -coqtop.byte -coqtop.opt -minicoq -coqdep -coq_makefile -gallina -coq-tex -coq-extraction -coq-interface -parser -parser.opt -coq_vo2xml -coq-interface.opt -coqide.byte -coqide.opt -coqtopnew.opt -coqtopnew.byte -coqwc -coqdoc |
