Re: [sage-devel] Re: Graceful shutdown of patchbot

2016-09-21 Thread Jeroen Demeyer
On 2016-09-21 13:55, Frédéric Chapoton wrote: This is because the patchbot called with "sage -patchbot" needs currently to be launched from the branch of https://trac.sagemath.org/ticket/20736 Well, *you* (or anybody else) could help by reviewing that ticket. -- You received this message

Re: [sage-devel] Re: Graceful shutdown of patchbot

2016-09-21 Thread John Cremona
On 21 September 2016 at 12:55, Frédéric Chapoton wrote: > This is because the patchbot called with "sage -patchbot" needs currently to > be launched from the branch of https://trac.sagemath.org/ticket/20736 > > So you need to switch back to this branch.. This is very

Re: [sage-devel] Re: Graceful shutdown of patchbot

2016-09-21 Thread Frédéric Chapoton
This is because the patchbot called with "sage -patchbot" needs currently to be launched from the branch of https://trac.sagemath.org/ticket/20736 So you need to switch back to this branch.. This is very inconvenient, but as long as this ticket is not closed, thiis is like that. I would

Re: [sage-devel] Re: Graceful shutdown of patchbot

2016-09-21 Thread John Cremona
Related question: My patchbot-running machine was rebooted ungracefully. It's on a git branch called ticket_merged, and ./sage -patchbot fails with /home/jec/sagedev/src/bin/sage: line 271: /home/jec/sagedev/local/bin/patchbot/patchbot.py: No such file or directory How to recover? I was

[sage-devel] Re: Graceful shutdown of patchbot

2016-09-15 Thread Kwankyu Lee
> There is an option --count to say how many ticket to tests before to stop. > you may want to use that. > You may even change it in your json config file during the patchbot run > (not tested if this works to stop the bot) Ok. I will try that. Thanks. But Ctrl-C should not be very

[sage-devel] Re: Graceful shutdown of patchbot

2016-09-15 Thread Frédéric Chapoton
There is an option --count to say how many ticket to tests before to stop. you may want to use that. You may even change it in your json config file during the patchbot run (not tested if this works to stop the bot) But Ctrl-C should not be very problematic. Could you tell what kind of