diff --git a/.gitignore b/.gitignore index 712e889c4ae70949b1db334faca821aaa3f14e2f..79eb4c54495a83577b2e6790fbe5ea88948ea11e 100644 --- a/.gitignore +++ b/.gitignore @@ -173,4 +173,7 @@ scade-manuel.pdf src/TODO.org src/mli_save/ Makefile.version - +*.cmi +*.cmx +*.cmxs +*.o