Alexander Krauss wrote: > On 03/22/2011 10:17 PM, Makarius wrote: > >I also wonder about mirabelle -q, which produces strange messages in the > >regular makeall setup: > > > >http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Mirabelle/lib/scripts/mirabelle.pl#l134 > > > >http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Mirabelle/lib/scripts/mirabelle.pl#l139 > > > > > >Is this really intended, or just due to the confusing ne "" test?
Changeset d3404f32328a silences these two lines. I'm not quite sure whether they are necessary at all, but they might come in handy when running Mirabelle with several theories. Sascha _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
