Merge pull request xapi-project#13 from gaborigloi/update_gitignore

Add files to .gitignore after porting to OASIS
robhoes · May 4, 2017 · df56a07 · df56a07
2 parents 029d2d7 + 2a20e88
commit df56a07
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/.gitignore b/.gitignore
@@ -7,3 +7,17 @@
 *.cmx
 *.cmxs
 *.cmxa
+
+/_build
+/*.native
+/*.byte
+
+# OASIS
+/setup.log
+/setup.data
+/setup.ml
+/myocamlbuild.ml
+/_tags
+# DevFiles OASIS plugin:
+/Makefile
+/configure