From fc98718375759d0493e94d7760f626e9b3f2fb9e Mon Sep 17 00:00:00 2001
From: Xavier Clerc <xavier.clerc@inria.fr>
Date: Thu, 11 Dec 2014 17:03:18 +0100
Subject: Ignore *.vi files, just like *.vo files.

---
 .gitignore | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to '.gitignore')

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
-- 
cgit v1.2.3