--- 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