2 # See ./README.md for docs
11 log
"Usage: $0 GITHUB_REPO PR_NUMBER"
17 # Retry the API query this many times
19 # Start with 5 seconds, but double every retry
23 log
"Checking whether the pull request can be merged"
25 -H "Accept: application/vnd.github+json" \
26 -H "X-GitHub-Api-Version: 2022-11-28" \
27 "/repos/$repo/pulls/$prNumber")
29 # Non-open PRs won't have their mergeability computed no matter what
30 state
=$
(jq
-r .state
<<< "$prInfo")
31 if [[ "$state" != open
]]; then
32 log
"PR is not open anymore"
36 mergeable
=$
(jq
-r .mergeable
<<< "$prInfo")
37 if [[ "$mergeable" == "null" ]]; then
38 if (( retryCount
== 0 )); then
39 log
"Not retrying anymore. It's likely that GitHub is having internal issues: check https://www.githubstatus.com/"
42 (( retryCount
-= 1 )) || true
44 # null indicates that GitHub is still computing whether it's mergeable
45 # Wait a couple seconds before trying again
46 log
"GitHub is still computing whether this PR can be merged, waiting $retryInterval seconds before trying again ($retryCount retries left)"
47 sleep "$retryInterval"
49 (( retryInterval
*= 2 )) || true
56 if [[ "$mergeable" == "true" ]]; then
57 log
"The PR can be merged"
58 jq
-r .merge_commit_sha
<<< "$prInfo"
60 log
"The PR has a merge conflict"