diff options
| author |  Xavier Clerc <xavier.clerc@inria.fr> | 2014-12-11 17:03:18 +0100 |
|---|---|---|
| committer | Xavier Clerc <xavier.clerc@inria.fr> | 2014-12-11 17:03:18 +0100 |
| commit | fc98718375759d0493e94d7760f626e9b3f2fb9e (patch) | |
| tree | 9bfb7e21ce6e6d6ded25f8aefd35f4d288a08dc9 /.gitignore | |
| parent | 2041981770992285798183754987eab25bf95181 (diff) | |
Ignore *.vi files, just like *.vo files.
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore index 1820bf7f9..cb728ea75 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,7 @@ *.glob *.d *.d.raw +*.vi *.vo *.cm* *.annot @@ -158,4 +159,4 @@ dev/myinclude \#*\# # coqide generated files (when testing) -*.crashcoqide
\ No newline at end of file +*.crashcoqide |