On 17.12.2012 12:13, Makarius wrote:
We merely need to learn where to draw the line. For example, the isatest settings have greatly benefitted from being exposed in Admin/isatest/settings under official version control. Before it was always a guess in the dark what isatest was using in a failed test in the first place.
AFAIK this is still a problem with mira. Unless something changed recently, mira uses the version of isabelle/Admin/mira.py present when
the mira daemon was started, which is not a very well-defined notion. -- Lars _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
