aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2014-09-21 10:57:04 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2014-09-21 10:57:04 +0200
commit0899260c83d012af0a50d4099abf039f53d61fbb (patch)
tree4f789cfef620d8245b8663fc7b9f7dcc956867f0 /extraction
parent55d08b039b9683eedd89e2dee17bc2a347057633 (diff)
downloadcompcert-kvx-0899260c83d012af0a50d4099abf039f53d61fbb.tar.gz
compcert-kvx-0899260c83d012af0a50d4099abf039f53d61fbb.zip
Add .gitignore files.
Diffstat (limited to 'extraction')
-rw-r--r--extraction/.gitignore5
1 files changed, 5 insertions, 0 deletions
diff --git a/extraction/.gitignore b/extraction/.gitignore
new file mode 100644
index 00000000..92df2ef4
--- /dev/null
+++ b/extraction/.gitignore
@@ -0,0 +1,5 @@
+# Caml files generated by extraction
+*.mli
+*.ml
+# Extraction timestamp
+STAMP