# HG changeset patch
# User Glenn Morris <rgm@gnu.org>
# Date 1276313755 25200
# Node ID f282583957c5167e2a82ce2338e1fc7ec0f7bb6a
# Parent  506ba691342fa34d9169da0b57f88b4559e9a429
* Makefile.in (install-arch-indep): Delete any old info .gz files first.

diff -r 506ba691342f -r f282583957c5 ChangeLog
--- a/ChangeLog	Fri Jun 11 23:26:13 2010 +0200
+++ b/ChangeLog	Fri Jun 11 20:35:55 2010 -0700
@@ -1,3 +1,7 @@
+2010-06-12  Glenn Morris  <rgm@gnu.org>
+
+	* Makefile.in (install-arch-indep): Delete any old info .gz files first.
+
 2010-06-11  Glenn Morris  <rgm@gnu.org>
 
 	* configure.in (--without-compress-info): New option.
diff -r 506ba691342f -r f282583957c5 Makefile.in
--- a/Makefile.in	Fri Jun 11 23:26:13 2010 +0200
+++ b/Makefile.in	Fri Jun 11 20:35:55 2010 -0700
@@ -583,6 +583,7 @@
 	        ${INSTALL_DATA} $$f $(DESTDIR)${infodir}/$$f; \
 	        chmod a+r $(DESTDIR)${infodir}/$$f; \
 	        if [ -n "${GZIP_INFO}" ] && [ -n "${GZIP_PROG}" ]; then \
+	          rm -f $(DESTDIR)${infodir}/$$f.gz; \
 	          ${GZIP_PROG} -9n $(DESTDIR)${infodir}/$$f; \
 	        else true; fi; \
 	      done; \
@@ -606,6 +607,7 @@
 	   ${INSTALL_DATA} ${mansrcdir}/$${page} $(DESTDIR)${man1dir}/$${page}; \
 	   chmod a+r $(DESTDIR)${man1dir}/$${page}; \
 	   if [ -n "${GZIP_INFO}" ] && [ -n "${GZIP_PROG}" ]; then \
+	     rm -f $(DESTDIR)${man1dir}/$${page}.gz; \
 	     ${GZIP_PROG} -9n $(DESTDIR)${man1dir}/$${page}; \
 	   else true; fi ); \
 	done