(realclean): Remove Info files.

diff --git a/compatMakefile b/compatMakefile
index 9ee55b1b80d6d0e89b079d136c2aac2be3cb32a1..188fb30020432a08a02cc295859dbe695674d439 100644 (file)
--- a/compatMakefile
+++ b/compatMakefile
@@ -249,6 +249,7 @@ distclean: clean glob-realclean
        -rm -f make.?? make.??s make.log make.toc make.*aux
        -rm -f loadavg.c
 realclean: distclean
+       -rm -f make.info*
 mostlyclean: clean
 
 .PHONY: glob-clean glob-realclean