[isabelle-dev] Repository and Wiki [was: push request (Sublist.thy)]

Lars Noschinski noschinl at in.tum.de
Mon Dec 17 12:18:56 CET 2012


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



More information about the isabelle-dev mailing list