:wave: I just posted a feature request: <GitHub a...
# pulumi-cloud
p
l
Aaron's comment is the big blocker to this: can a push event know which PR caused it?
And the related question would be: what happens when a push event is triggered without a PR? I know it shouldn't ever, but it is possible, so therefore, it will happen just after you create something that utterly depends on it not happening.
p
My impression is that that info is not right at hand in that context. I have an action where I need to retrieve this myself, so I’ve been thinking about this. I think the easiest way to determine the PR would be by examining the title (first line) of the commit message of the HEAD commit. Usually it contains
#nn
e.g.
#42
being the PR number. So it shouldn’t be hard to use a regex to retrieve that and then you can retrieve more details on the PR via the GitHub API, if needed.
Ah I see the comment now
I’ll copy-pasta that above
thanks
l
It's not unambiguous, unfortunately. It would be possible, for example, to have two PRs with the same commit and the same comment.
Complete straw man, of course.. but I think it would be possible to break stuff fairly easily when relying on that sort of solution. The GitHub API would need to provide some explicit link back to the PR.
p
Yes, I agree. It’s not great. I’ll try to look into this more.
l
So imo Aaron's response hits the nail on the head: a feature request to GitHub to add that info into the merge push would be great. In fact, I bet that the feature is already there, or the request is...
It certainly would be a helpful feature in lots of other cases.
p
agreed
l
Looks good.. there's not much chance of a commit having more than one PR associated with it.. thought it'll probably happen eventually...