[isabelle-dev] Mirabelle and load path

[Sascha Boehme]

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