Tobias Nipkow wrote:
Brian's latest patch "remove HOLCF from build script, since it no longer
works" has an unfortunate effect: the isabelle script now terminates
immediately with
Bad Isabelle component: "/Users/nipkow/isabelle/src/HOLCF"
Which is annoying, given that I do not want to use HOLCF at all.
Can I do something to avoid this?

The root /etc/components still mentions src/HOLCF. This should either be removed or changed to src/HOL/HOLCF. I removed it for now in 04d44a20fccf.

Alex
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to