diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/.cvsignore | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/.cvsignore b/dev/.cvsignore index e494556aa6..48df473800 100644 --- a/dev/.cvsignore +++ b/dev/.cvsignore @@ -1,3 +1,3 @@ other -ocamldebug-v7 -debug_*
\ No newline at end of file +ocamldebug-coq +debug_* |
