Hi Ben, On 11/17/25 3:00 PM, Ben Boeckel wrote:
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.
We rebase our commits, so I don't think we'd be able to access that info. However, I think you're right that just doing an API call on the commit link would give us that pull-request number, or even a little bit of HTML scraping :) But for now this is basically a shell script, so it might be a little out there. I think we are considering eventually moving this to another one of our tools which could do these more involved procedures - I think it would have to wait until then.
Arthur
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
OpenPGP_0x1B3465B044AD9C65.asc
Description: OpenPGP public key
OpenPGP_signature.asc
Description: OpenPGP digital signature
