Hi, On Tue, Jan 02, 2018 at 04:10:47PM +0100, Erik Bray wrote: > 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.
I was not proposing to "just" stop, but i think that polluting all the ticket's reports because of an unrelated issue is not productive. If some patchbot do not report success on the develop branch (ticket 0), then it should stop testing tickets, this is what i meant. I personally check my patchbots "by hand" when i see them stopped, and report bugs when necessary, though i admit there should be other ways to get informed that they went wrong, as Erik suggests. > 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. Note that ticket 0 has a dedicated page, where we can inspect patchbot issues: https://patchbot.sagemath.org/ticket/0/ so it should be possible to parse it, or to have the patchbot server generate a dedicated page that is more parsable (e.g. RSS feed, json, whatever). Ciao, Thierry > 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. -- 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.
