On Wed, Mar 24, 2010 at 7:18 AM, Brian Huffman <[email protected]> wrote: > I tried grepping everywhere I can think of,
I didn't move far enough up the directory tree: I found the offending line in /etc/components. - Brian _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
