[ "$old_head" = "$new_head" ] ||
[ "$(git diff ${old_head}.. | wc -c)" -eq 0 ] || {
- git push -f "$build_host":"$build_dir" master:refs/heads/next || {
+ git push -f "${build_host}${build_host:+:}${build_dir}" master:refs/heads/next || {
echo git push failed 1>&2
bash -i || exit
}
[ "$old_head" = "$new_head" ] ||
[ "$(git diff ${old_head}.. | wc -c)" -eq 0 ] || {
- git push -f "$build_host":"$build_dir" master:refs/heads/next || {
+ git push -f "${build_host}${build_host:+:}${build_dir}" master:refs/heads/next || {
echo git push failed 1>&2
bash -i || exit
}