diff --git a/mps/.gitignore b/mps/.gitignore index 311153ef7d6..8f7c5d938a1 100644 --- a/mps/.gitignore +++ b/mps/.gitignore @@ -11,6 +11,7 @@ # Autoconf and Automake output Makefile autom4te.cache +aclocal.m4 config.log config.status .deps