aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorGuillaume Melquiond <guillaume.melquiond@inria.fr>2021-12-04 11:45:24 +0100
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-04-25 16:38:45 +0200
commit111fda0f629b68138f9d816a4e6a86f7c292f2a2 (patch)
tree485236387014b3036ca877425534572f2a5077eb
parent9aacc59135071a979623ab177819cdbe9ce27056 (diff)
downloadcompcert-111fda0f629b68138f9d816a4e6a86f7c292f2a2.tar.gz
compcert-111fda0f629b68138f9d816a4e6a86f7c292f2a2.zip
Ignore .coq-native directories.
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 99facd7e..e735fec3 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,6 +13,7 @@
.*.aux
*.cmti
*.cmt
+.coq-native
# Emacs saves
*~
# Executables and configuration