@@ -16,19 +16,32 @@ jobs:
1616 pr : ${{ steps.get-pr.outputs.pr }}
1717 steps :
1818 - id : get-commit-hash
19- run : echo "commit=${GITHUB_SHA}" >> "$GITHUB_OUTPUT"
20- - name : Check commit hash and PR
2119 run : |
20+ echo "commit=${GITHUB_SHA}" >> "$GITHUB_OUTPUT"
2221 echo "Commit hash: ${GITHUB_SHA}"
23- echo "Pull request for the commit is below:"
24- gh pr list --search "${GITHUB_SHA}" --state merged --repo mmtk/mmtk-core
25- env :
26- GITHUB_TOKEN : ${{ secrets.GITHUB_TOKEN }}
2722 - id : get-pr
2823 run : |
29- PR_NUMBER=$(gh pr list --search "${GITHUB_SHA}" --state merged --repo mmtk/mmtk-core --json number --jq '.[0].number')
30- echo "pr=$PR_NUMBER" >> "$GITHUB_OUTPUT"
31- echo "Output pr=$PR_NUMBER"
24+ for n in {1..5}; do
25+ echo "Wait 30s then try get the pull request number"
26+ sleep 30
27+
28+ echo "Pull request for the commit is below:"
29+ gh pr list --search "${GITHUB_SHA}" --state merged --repo mmtk/mmtk-core
30+ echo "Pull request for the commit is above."
31+
32+ PR_NUMBER=$(gh pr list --search "${GITHUB_SHA}" --state merged --repo mmtk/mmtk-core --json number --jq '.[0].number')
33+
34+ if [ -n "$PR_NUMBER" ] && [ "$PR_NUMBER" != "null" ]; then
35+ echo "Found PR: $PR_NUMBER"
36+ echo "pr=$PR_NUMBER" >> "$GITHUB_OUTPUT"
37+ echo "Output pr = $PR_NUMBER"
38+ exit 0
39+ fi
40+
41+ echo "PR not found, retrying..."
42+ done
43+ echo "We can't find the merged PR for ${GITHUB_SHA}"
44+ exit 1
3245 env :
3346 GITHUB_TOKEN : ${{ secrets.GITHUB_TOKEN }}
3447
0 commit comments