diff options
| author | Silvan Mosberger <contact@infinisil.com> | 2023-12-01 04:47:17 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-12-01 04:47:17 +0100 |
| commit | ac01ff7146a43d5fe1624bc41c6e452f4d202e10 (patch) | |
| tree | b6cae684c5e302bc819a42b5d57102c623db446c /.github | |
| parent | 80d1486870e6189e9471b0de7482d7fbb4fb16e6 (diff) | |
| parent | 5e0644896dce54c876df00c69fc824e3614fe61c (diff) | |
Merge pull request #270496 from tweag/by-name-backoff
workflows/check-by-name: Limited and exponential retries
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/check-by-name.yml | 25 |
1 files changed, 21 insertions, 4 deletions
diff --git a/.github/workflows/check-by-name.yml b/.github/workflows/check-by-name.yml index 22700e0f6d441..8ae66e246732f 100644 --- a/.github/workflows/check-by-name.yml +++ b/.github/workflows/check-by-name.yml @@ -16,6 +16,9 @@ jobs: # This is x86_64-linux, for which the tool is always prebuilt on the nixos-* channels, # as specified in nixos/release-combined.nix runs-on: ubuntu-latest + # This should take 1 minute at most, but let's be generous. + # The default of 6 hours is definitely too long + timeout-minutes: 10 steps: - name: Resolving the merge commit env: @@ -23,6 +26,11 @@ jobs: run: | # This checks for mergeability of a pull request as recommended in # https://docs.github.com/en/rest/guides/using-the-rest-api-to-interact-with-your-git-database?apiVersion=2022-11-28#checking-mergeability-of-pull-requests + + # Retry the API query this many times + retryCount=3 + # Start with 5 seconds, but double every retry + retryInterval=5 while true; do echo "Checking whether the pull request can be merged" prInfo=$(gh api \ @@ -33,10 +41,19 @@ jobs: mergedSha=$(jq -r .merge_commit_sha <<< "$prInfo") if [[ "$mergeable" == "null" ]]; then - # null indicates that GitHub is still computing whether it's mergeable - # Wait a couple seconds before trying again - echo "GitHub is still computing whether this PR can be merged, waiting 5 seconds before trying again" - sleep 5 + if (( retryCount == 0 )); then + echo "Not retrying anymore, probably GitHub is having internal issues" + exit 1 + else + (( retryCount -= 1 )) || true + + # null indicates that GitHub is still computing whether it's mergeable + # Wait a couple seconds before trying again + echo "GitHub is still computing whether this PR can be merged, waiting $retryInterval seconds before trying again ($retryCount retries left)" + sleep "$retryInterval" + + (( retryInterval *= 2 )) || true + fi else break fi |