Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[fix] Let GitHub tell us which PR (or PRs) this workflow run is for
This fixes a bug whence someone else pushes to a PR branch than whomever opened it, and then the “bot” used to get confused. - Use `${{ github.event.workflow_run.pull_requests }}` as seen in https://docs.github.com/en/developers/webhooks-and-events/webhooks/webhook-events-and-payloads#webhook-payload-object-1 — Only it's an array (for the unlikely case that multiple PRs are open on the same branch at the same time); so pass it through `toJSON()` - For the same reason (need to tolerate the multiple PRs case), change the call to `upsertComment` to happen in a loop.
- Loading branch information