File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -64,12 +64,14 @@ jobs:
6464 git commit -m "diagnosis: update $host report (from #$ISSUE)"
6565 git push -f origin "$branch"
6666
67- # One PR per host branch: open it the first time, reuse it after.
68- url=$(gh pr view "$branch" --json url --jq .url 2>/dev/null || true)
67+ # One open PR per host branch: reuse it while it is open, open a new
68+ # one once the previous report has merged (a merged/closed PR for the
69+ # branch must not suppress the next submission).
70+ url=$(gh pr list --head "$branch" --state open --json url --jq '.[0].url // empty')
6971 if [ -z "$url" ]; then
7072 url=$(gh pr create --base main --head "$branch" \
7173 --title "diagnosis: $mode host report" \
72- --body "Updates \`$file\` from the playground Diagnosis . The compatibility matrix is regenerated from the reports at build time.")
74+ --body "Updates \`$file\` from the diagnosis in #$ISSUE . The compatibility matrix is regenerated from the reports at build time.")
7375 fi
7476
7577 gh issue comment "$ISSUE" --body "Filed in $url"
You can’t perform that action at this time.
0 commit comments