| changeset 5398 | 81936a99a3b0 |
| parent 5367 | 33f81e980c93 |
| child 5403 | aa04ac8bfeae |
| 5397:034ed25535b9 | 5398:81936a99a3b0 |
|---|---|
45 if [ -f "$BIN" -a -x "$BIN" ]; then |
45 if [ -f "$BIN" -a -x "$BIN" ]; then |
46 B=$DIR/$(basename $BIN) |
46 B=$DIR/$(basename $BIN) |
47 echo "install $B" |
47 echo "install $B" |
48 echo "#!$BASH" >$B || fail "Cannot write file: $B" |
48 echo "#!$BASH" >$B || fail "Cannot write file: $B" |
49 echo >>$B |
49 echo >>$B |
50 echo "$BIN \"\$@\"" >>$B |
50 echo "exec $BIN \"\$@\"" >>$B |
51 chmod +x $B |
51 chmod +x $B |
52 fi |
52 fi |
53 done |
53 done |