# 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