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

diff --git a/build-support/factor.sh b/build-support/factor.sh
index d090433d98e2fe705bcdc39826292362d0c65f49..2f8745aeef878c13aaf1a57fdde04dfe0703fb10 100755 (executable)
--- a/build-support/factor.sh
+++ b/build-support/factor.sh
@@ -347,8 +347,8 @@ update_script_name() {
 
 update_script() {
     update_script=`update_script_name`
-    
-    echo "#!/bin/sh" >"$update_script"
+       bash_path=`which bash`
+    echo "#!$bash_path" >"$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" \
         >>"$update_script"