If we move our issues to github, which I do still want to do, then wouldn't this be pointless since issues and pull requests are basically the same thing?
Aaron Meurer On Nov 22, 2013, at 7:32 AM, Sergey Kirpichev <skirpic...@gmail.com> wrote: On Friday, August 9, 2013 7:40:50 PM UTC+4, Ondřej Čertík wrote: > > I propose to create an issue for old pull requests and close them with > some kind words and encourage the author to reopen it if he or she > starts working on it again. > Seems very reasonable and actual. > Proposal for policy: our PR queue should be for active work. If PR is > not ready to merge and nobody is working on it, we should move it out > of our PR queue and move it to our issues --- with a convenient tag > like "pull-request", so that people who would like to take over them > can do that from issues. > The only objection: you should clarify that means "nobody is working on". Perhaps, iff PR has been reviewed (not positively) and the author does not respond to reviewer(s) for a given time (month?). -- You received this message because you are subscribed to the Google Groups "sympy" group. To unsubscribe from this group and stop receiving emails from it, send an email to sympy+unsubscr...@googlegroups.com. To post to this group, send email to sympy@googlegroups.com. Visit this group at http://groups.google.com/group/sympy. For more options, visit https://groups.google.com/groups/opt_out. -- You received this message because you are subscribed to the Google Groups "sympy" group. To unsubscribe from this group and stop receiving emails from it, send an email to sympy+unsubscr...@googlegroups.com. To post to this group, send email to sympy@googlegroups.com. Visit this group at http://groups.google.com/group/sympy. For more options, visit https://groups.google.com/groups/opt_out.
