Add gitignore

dannywillems · May 23, 2016 · 17a5ebd · 17a5ebd
1 parent 058d2b0
commit 17a5ebd
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/.gitignore b/.gitignore
@@ -0,0 +1,4 @@
+*.cma
+*.cmo
+*.cmi
+*.ml