From 471be744b615eae8b697d171acf874054389c4e4 Mon Sep 17 00:00:00 2001
From: Doug Coleman <doug.coleman@gmail.com>
Date: Sun, 10 Jan 2010 22:42:26 -0600
Subject: [PATCH] Use the bash path instead of /bin/sh for running a bash
 script

---
 build-support/factor.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/build-support/factor.sh b/build-support/factor.sh
index d090433d98..2f8745aeef 100755
--- 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"