aboutsummaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
authorYann Herklotz <git@ymhg.org>2019-10-02 19:48:57 +0100
committerGitHub <noreply@github.com>2019-10-02 19:48:57 +0100
commit0047efca720eadc6d5a91b99318be985380b5fd6 (patch)
treee623bf121a367c6416a788034953106c9542efcc /.gitignore
downloadvericert-0047efca720eadc6d5a91b99318be985380b5fd6.tar.gz
vericert-0047efca720eadc6d5a91b99318be985380b5fd6.zip
Initial commit
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore30
1 files changed, 30 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..f25a61d
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,30 @@
+.*.aux
+*.a
+*.cma
+*.cmi
+*.cmo
+*.cmx
+*.cmxa
+*.cmxs
+*.glob
+*.ml.d
+*.ml4.d
+*.mli.d
+*.mllib.d
+*.mlpack.d
+*.native
+*.o
+*.v.d
+*.vio
+*.vo
+.coq-native/
+.csdp.cache
+.lia.cache
+.nia.cache
+.nlia.cache
+.nra.cache
+csdp.cache
+lia.cache
+nia.cache
+nlia.cache
+nra.cache