diff options
| author | Erich Eckner <git@eckner.net> | 2017-05-31 11:16:01 +0200 |
|---|---|---|
| committer | Erich Eckner <git@eckner.net> | 2017-05-31 11:16:01 +0200 |
| commit | 8c2c3ec8abbc89a708c617f99191645f95c64e78 (patch) | |
| tree | bd6c959a461674280b749d7457c2ddb88782eff5 /bin/build-packages | |
| parent | cf8b959ce1cfeb8028ecd2e1b6b46c02256484f0 (diff) | |
| download | builder-8c2c3ec8abbc89a708c617f99191645f95c64e78.tar.xz | |
bin/build-packages: handle busy build server in case of tried error report
Diffstat (limited to 'bin/build-packages')
| -rwxr-xr-x | bin/build-packages | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/bin/build-packages b/bin/build-packages index e66afdb..f064556 100755 --- a/bin/build-packages +++ b/bin/build-packages @@ -216,11 +216,13 @@ while [ ${count} -ne 0 ]; do done if ! ${success}; then - ssh \ + while ! ssh \ -i "${master_build_server_identity}" \ -p "${master_build_server_port}" \ "${master_build_server_user}@${master_build_server}" \ - 'return-assignment' "${package}" "${git_revision}" "${mod_git_revision}" "${repository}" 'ERROR' + 'return-assignment' "${package}" "${git_revision}" "${mod_git_revision}" "${repository}" 'ERROR'; do + sleep $[15+$RANDOM%30] + done if ${exit_after_failure}; then >&2 echo 'Build failed, exiting now' exit |