I bet the cause of this sometimes is with PRs where github detected they
were merged and closed them automatically.
We make a point of adding the merged comment anyway but it's easier for
this to fall into a crack if we don't even need to close the PR.
On 8/29/13 3:55 AM, Jaikiran Pai wrote:
Yeah, we do make it a point to add a comment which says
whenever the PR gets merged. It might have been an oversight that
certain PRs didn't receive such comments.But yes, we will continue to
follow this process of adding a comment.
On Thursday 29 August 2013 02:21 PM, Darran Lofthouse wrote:
> On 28/08/13 20:47, Brian Stansberry wrote:
>> If you have a JIRA assigned to you and it's in "Pull Request Sent"
>> status in JIRA but you know the PR has been merged and the issue can
>> be resolved, can you resolve the JIRA, please?
> Can we make sure that when pull requests are merged there is also always
> a closing comment added to say it is closed?
> I think it is happening now but in the past sometimes PRs were merged
> and closed without comment and then there was no notification received
> to remind you to close Jira / clean up branches used for the PR.
>> I normally make an effort to do this when I merge PRs, as do the other
>> mergers, but it's been slipping a bit lately. So if folks can take care
>> of their own that will clean JIRA up a bit.
> wildfly-dev mailing list
wildfly-dev mailing list
Principal Software Engineer
JBoss by Red Hat