update to_build_host a bit

[next-scripts] / do_revert

diff --git a/do_revert b/do_revert
index d5e585dd3cc2a61e97f7c4091251f445fc0ac55d..f56960a6288c8c3eda81b732c5eca9cc911e02c9 100755 (executable)
--- a/do_revert
+++ b/do_revert
@@ -28,7 +28,7 @@ GIT_EDITOR=: execute git revert $rev || exit 1
 
 $no_build && exit 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
 }