# HG changeset patch
# User Richard M. Stallman <rms@gnu.org>
# Date 738540775 0
# Node ID 2852a2acef363b85d4308ef760541e8efb33056b
# Parent  241c63a9aaa1ff8e828866588dbb9acec7be04f1
(do-install): Delete the dest dir, not the source dir,
when they are different.

diff -r 241c63a9aaa1 -r 2852a2acef36 Makefile.in
--- a/Makefile.in	Thu May 27 22:02:16 1993 +0000
+++ b/Makefile.in	Thu May 27 22:12:55 1993 +0000
@@ -332,7 +332,7 @@
 	-set ${COPYDESTS} ; \
 	 for dir in ${COPYDIR} ; do \
 	   if [ `(cd $$1 ; pwd)` != `(cd $${dir} ; pwd)` ] ; then \
-	     rm -rf $${dir} ; \
+	     rm -rf $$1 ; \
 	   fi ; \
 	 done
 	-set ${COPYDESTS} ; \