The other thing that I just noticed can be a problem is that it is not clear if a closed pull request is closed because it was merged or because a better patch was needed (unless the pull was exactly merged, in which case it says "merged" at the top). So if you are closing a pull request for whatever reason, you should always include a comment saying why it was closed (because the patch was pushed or for some other reason). If it closes automatically, again, it will say "merged" at the top, so you don't need to worry about it.
Aaron Meurer On Apr 6, 11:07 am, Ondrej Certik <ond...@certik.cz> wrote: > On Wed, Apr 6, 2011 at 9:03 AM, Vinzent Steinberg > > <vinzent.steinb...@googlemail.com> wrote: > > On 6 Apr., 00:32, Ondrej Certik <ond...@certik.cz> wrote: > >> > I think the suggestion is to not open a new one but to reopen the same > >> > one. > > >> Yes. > > > Alright, this definitely makes sense. The only drawback I see is that > > we can't tell the difference between a closed unfinished and a closed > > finished pull request easily. > > That's true (e.g. some things could be improved at github), but then > again, pull requests are not an issue tracker. Pull requests are a > tool for "people who want their code in, and are willing and ready to > work on it". And if the original author becomes busy/losts interest, > then we simply close it and create an issue for it, so that his work > is not lost, but it doesn't obstruct the other pull requests from > people who are ready to work on it. > > Ondrej -- You received this message because you are subscribed to the Google Groups "sympy" group. To post to this group, send email to sympy@googlegroups.com. To unsubscribe from this group, send email to sympy+unsubscr...@googlegroups.com. For more options, visit this group at http://groups.google.com/group/sympy?hl=en.
