Hi Roman, The problem is still have someone forget to close PR, and we can't contact him only using email notification.
As for your suggestion, could you please share with us the exact steps how to do it? Thanks. On Thu, Sep 8, 2016 at 2:13 PM, Roman Shaposhnik <[email protected]> wrote: > On Wed, Sep 7, 2016 at 11:08 PM, Lei Chang <[email protected]> wrote: > > @ming, there is a discussion on this mailing list before about what > should > > be included in the commit message. > > > > Appending "close #" makes the commit message very messy. > > > > So the conclusion at that time is to not append "close #" to a commit > > message. > > > > If someone forgets closing a pull request, looks better to add a reminder > > to the pull request. > > Not to reopen that old discussion, but have you guys considered adding > it to the body of the commit? That way it won't mess up git log and such > but will still have the desired effect. > > Thanks, > Roman. >
