On 2017-12-24 17:07, Thierry wrote:
It should stop.
That's not a solution. If it just stops, then nobody would notice that there is a problem. And since there are regularly problems, running a patchbot would require a lot more work. You would just kill all patchbots, which is much worse than the situation that we currently have.
-- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To post to this group, send email to sage-devel@googlegroups.com. Visit this group at https://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/d/optout.
