# HG changeset patch
# User Richard M. Stallman <rms@gnu.org>
# Date 889146777 0
# Node ID ef9a01b67c87718476affb3f999c479e1f90c168
# Parent  39d081df364398fca5d556f4b20f05bb1bf482d7
(install): Use INSTALL_STRIP with INSTALL_PROGRAM for the utilities.

diff -r 39d081df3643 -r ef9a01b67c87 lib-src/Makefile.in
--- a/lib-src/Makefile.in	Thu Mar 05 04:00:53 1998 +0000
+++ b/lib-src/Makefile.in	Fri Mar 06 01:12:57 1998 +0000
@@ -284,7 +284,7 @@
 	@echo
 	@echo "Installing utilities for users to run."
 	for file in ${INSTALLABLES} ; do \
-	  $(INSTALL_PROGRAM) $${file} ${bindir}/$${file} ; \
+	  $(INSTALL_PROGRAM) $(INSTALL_STRIP) $${file} ${bindir}/$${file} ; \
 	  chmod a+rx ${bindir}/$${file}; \
 	done
 	for file in ${INSTALLABLE_SCRIPTS} ; do \