On Mon, Dec 25, 2017 at 3:12 AM, Jeroen Demeyer <[email protected]> wrote: > 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.
It would help if patchbots had some kind of reporting mechanism, such as to send an e-mail to its owner. This might be better implemented on the server side though, or as a separate service that just polls the patchbot server for results and notifies the appropriate people. I've been meaning to write something to do the latter and set it up just as a cron job or something to alert me when a patchbot I care about starts failing to build. -- 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 [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/d/optout.
