# HG changeset patch
# User wenzelm
# Date 904241743 -7200
# Node ID 81936a99a3b043fc8dbdce86136b2cd70f266a48
# Parent  034ed25535b94a54c7581dfeccbc0c54c26eaf5c
exec;

diff -r 034ed25535b9 -r 81936a99a3b0 lib/Tools/install
--- a/lib/Tools/install	Thu Aug 27 18:46:57 1998 +0200
+++ b/lib/Tools/install	Thu Aug 27 20:15:43 1998 +0200
@@ -47,7 +47,7 @@
     echo "install $B"
     echo "#!$BASH" >$B || fail "Cannot write file: $B"
     echo >>$B
-    echo "$BIN \"\$@\"" >>$B
+    echo "exec $BIN \"\$@\"" >>$B
     chmod +x $B
   fi
 done