I think we should offer a solution for this problem, even if the solution is not good enough. If you find a better solution for it, we can enhance it afterward.
On Thu, Sep 8, 2016 at 3:16 PM, Ming Li <[email protected]> wrote: > 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. >> > >
