Dear all,

A patchbot is supposed to run forever, but realistically I should stop it 
from time to time. Pushing ctrl-c stops the patchbot abruptly, and the 
subsequent run seems sometimes to show somewhat erroneous behavior, perhaps 
due to the spurious state of the files.

Is there a way to stop the patchbot gracefully? Or am I worrying too much 
and ctrl-c is just ok?

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 post to this group, send email to
Visit this group at
For more options, visit

Reply via email to