aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-22 21:30:04 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-22 21:30:04 +0000
commitf6dd0d9ef10fe8d9b742001fef6f68f06ac05218 (patch)
tree6155dd587056c7c9e665e9f0e3098dff295ed1c2 /.gitignore
parent6b908b5185a55a27a82c2b0fce4713812adde156 (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--.gitignore1
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