steve
/
factor
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Use the bash path instead of /bin/sh for running a bash script

db4
Doug Coleman 2010-01-10 22:42:26 -06:00
parent 8ce6ee04fc
commit 782d91f927
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
build-support/factor.sh
View File

@ -347,8 +347,8 @@ update_script_name() {
update_script() { update_script() {
update_script=`update_script_name` update_script=`update_script_name`
bash_path=`which bash`
echo "#!/bin/sh" >"$update_script" echo "#!$bash_path" >"$update_script"
echo "git pull \"$GIT_URL\" master" >>"$update_script" echo "git pull \"$GIT_URL\" master" >>"$update_script"
echo "if [[ \$? -eq 0 ]]; then exec \"$0\" $SCRIPT_ARGS; else echo \"git pull failed\"; exit 2; fi" \ echo "if [[ \$? -eq 0 ]]; then exec \"$0\" $SCRIPT_ARGS; else echo \"git pull failed\"; exit 2; fi" \
>>"$update_script" >>"$update_script"