Skip to content

Allow retry in get-merged-pr #1427

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
qinsoon merged 3 commits into from
Dec 3, 2025
Merged

Allow retry in get-merged-pr #1427

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
580b56f
Allow retry in get-merged-pr
qinsoon Dec 2, 2025
33f73e8
Merge branch 'master' into retry-get-merged-pr
qinsoon Dec 2, 2025
84df4f4
Echo gh pr list before each retry
qinsoon Dec 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 22 additions & 9 deletions .github/workflows/auto-merge.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,19 +16,32 @@ jobs:
pr: ${{ steps.get-pr.outputs.pr }}
steps:
- id: get-commit-hash
run: echo "commit=${GITHUB_SHA}" >> "$GITHUB_OUTPUT"
- name: Check commit hash and PR
run: |
echo "commit=${GITHUB_SHA}" >> "$GITHUB_OUTPUT"
echo "Commit hash: ${GITHUB_SHA}"
echo "Pull request for the commit is below:"
gh pr list --search "${GITHUB_SHA}" --state merged --repo mmtk/mmtk-core
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- id: get-pr
run: |
PR_NUMBER=$(gh pr list --search "${GITHUB_SHA}" --state merged --repo mmtk/mmtk-core --json number --jq '.[0].number')
echo "pr=$PR_NUMBER" >> "$GITHUB_OUTPUT"
echo "Output pr=$PR_NUMBER"
for n in {1..5}; do
echo "Wait 30s then try get the pull request number"
sleep 30

echo "Pull request for the commit is below:"
gh pr list --search "${GITHUB_SHA}" --state merged --repo mmtk/mmtk-core
echo "Pull request for the commit is above."

PR_NUMBER=$(gh pr list --search "${GITHUB_SHA}" --state merged --repo mmtk/mmtk-core --json number --jq '.[0].number')
Copy link
Collaborator

@wks wks Dec 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If we need to retry, it means something has gone wrong. For the ease of debugging, I suggest we print out the human-readable output before each try, and print out the value of $PR_NUMBER regardless whether it was successful.

Suggested change
PR_NUMBER=$(gh pr list --search "${GITHUB_SHA}" --state merged --repo mmtk/mmtk-core --json number --jq '.[0].number')
echo "Pull request for the commit is below:"
gh pr list --search "${GITHUB_SHA}" --state merged --repo mmtk/mmtk-core
PR_NUMBER=$(gh pr list --search "${GITHUB_SHA}" --state merged --repo mmtk/mmtk-core --json number --jq '.[0].number')
echo "Output pr=$PR_NUMBER"

Copy link
Member Author

@qinsoon qinsoon Dec 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.


if [ -n "$PR_NUMBER" ] && [ "$PR_NUMBER" != "null" ]; then
echo "Found PR: $PR_NUMBER"
echo "pr=$PR_NUMBER" >> "$GITHUB_OUTPUT"
echo "Output pr = $PR_NUMBER"
exit 0
fi

echo "PR not found, retrying..."
done
echo "We can't find the merged PR for ${GITHUB_SHA}"
exit 1
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

Expand Down