diff options
Diffstat (limited to 'ide/.cvsignore')
| -rw-r--r-- | ide/.cvsignore | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/ide/.cvsignore b/ide/.cvsignore deleted file mode 100644 index d047db846..000000000 --- a/ide/.cvsignore +++ /dev/null @@ -1,15 +0,0 @@ -lexer.ml -why_viewer -.depend -find_phrase.ml -highlight.ml -coqide -Makefile -test -config_lexer.ml -*.crashcoqide -config_parser.mli -config_parser.ml -utf8_convert.ml -*.v8 -undo.mli |