exec;

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