diff --git a/build.sh b/build.sh index 712257a0ad75b7441274147fd518d0e569281fac..90acb18c6e91815be1f4203a13680a39d6ac64d0 100755 --- a/build.sh +++ b/build.sh @@ -3,12 +3,17 @@ workspace=$1 -hostname=$(cat hostname) target=$3 comp_type=$4 branch=$5 with_gpu=$6 +if [ -f hostname ]; then + hostname=$(cat hostname) +else + hostname=$(hostname) +fi + if [ x"$branch" == x"" ]; then echo "Getting branch from git" branch=$(git ls-remote --heads origin | grep $(git rev-parse HEAD) | cut -d / -f 3)