On Mon, Nov 17, 2025 at 12:15:15 +0000, Marc Poulhiès via Gcc wrote: > So we moved to the "push"[2] context where we only see "new commits" > and github doesn't provide any pull request info. We would need to > find this ourself (using the same "GH magic" that can link a commit to > its pull request), which is completely possible, but not automatic. > > Also, I'm clearly not an expert, so I'd be happy to be proved wrong > here and provided with an example that makes this feature easy :)
Generally, the merge commit has the PR ID at least. A "simple" API call could get the PR metadata from there. At $DAYJOB, we make it a bit more rigorous with an explicit `Merge-request: !ID` trailer in the merge commit message. --Ben
