On 11/28/2012 10:11 AM, Lars Noschinski wrote:
mira still crashes from time to time. Sometimes, it is not a programming
error, but some external error condition which could maybe be handled
more gracefully:
Repository update fails: The repository corruptions yesterday and
some time ago caused a failed update (see attachment). Mira could
probabliy just go to sleep and try again later.
It should do that indeed. It is hard to distinguish network errors etc.
from other errors, but retrying a few times makes sense anyway.
For future changes it might be worth to keep in mind that the Mercurial
project considers the python interface as internal:
http://mercurial.selenic.com/wiki/MercurialApi
Right. This classification has somehow changed over the years. Back in
2008, use of the API was encouraged more. Switching to a CLI interface
requires a bit of work, though.
Alex
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
