diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-22 21:30:04 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-22 21:30:04 +0000 |
commit | f6dd0d9ef10fe8d9b742001fef6f68f06ac05218 (patch) | |
tree | 6155dd587056c7c9e665e9f0e3098dff295ed1c2 /.gitignore | |
parent | 6b908b5185a55a27a82c2b0fce4713812adde156 (diff) |
Added .native to .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16137 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to '.gitignore')
-rw-r--r-- | .gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore index 3bfcfb293..8418d9346 100644 --- a/.gitignore +++ b/.gitignore @@ -36,6 +36,7 @@ *.v.ps *.v.html *.stamp +*.native revision TAGS .DS_Store |