diff --git a/.gitignore b/.gitignore index 5dd1ae3..478d91f 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ *.cmo *.cmi +*.zip