diff --git a/.gitignore b/.gitignore index 52e72259..ab6fe08c 100644 --- a/.gitignore +++ b/.gitignore @@ -1,7 +1,3 @@ -*.o -*.cmi -*.cmx -*.annot *.exe *.err *.out