summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore2
1 files changed, 2 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index fee7bae..0a5d9d7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,5 +9,7 @@
*.cmxa
*.native
*.byte
+*.mllib
+*.mldylib
setup.log
setup.data