November 17, 2025 at 3:23 PM, "Arthur Cohen" <[email protected] mailto:[email protected]?to=%22Arthur%20Cohen%22%20%3Carthur.cohen%40embecosm.com%3E > wrote:
> > 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. Adding API calls was what I had in mind when I replied "I can have another try". In some other earlier prototype I already had such API calls :) Marc
