1 files changed, 1 insertions, 1 deletions

diff --git a/.hgignore b/.hgignore
index 862064ee..bcee8b16 100644
--- a/.hgignore
+++ b/.hgignore
@@ -39,7 +39,7 @@ demo/more/demo.*
 *.pdf
 *.ps
 *.toc
-*.m4
+aclocal.m4
 
 .depend
 Makefile.coq