Channels
#pulumi-cloud
Title
# pulumi-cloud
p
powerful-room-57148
05/26/2022, 3:46 PM👋 I just posted a feature request: GitHub app should post PR comments even when triggered by a push event
l
little-cartoon-10569
05/26/2022, 11:12 PMAaron'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
powerful-room-57148
05/26/2022, 11:15 PMMy 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#42Ah I see the comment now
I’ll copy-pasta that above
thanks
l
little-cartoon-10569
05/26/2022, 11:18 PMIt'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
powerful-room-57148
05/26/2022, 11:21 PMYes, I agree. It’s not great. I’ll try to look into this more.
l
little-cartoon-10569
05/26/2022, 11:22 PMSo 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
powerful-room-57148
05/26/2022, 11:22 PMagreed
l
little-cartoon-10569
05/26/2022, 11:33 PMLooks good.. there's not much chance of a commit having more than one PR associated with it.. thought it'll probably happen eventually...
6 Views