Hi,
I am using HOL4, yesterday I started receiving this error message
Exception raised Io {cause = SysErr ("No such file or directory", SOME
ENOENT), function = "TextIO.openIn", name = "/tmp/hol2207zVM"}
I am using HOL4 in the hol-mode, but when I use HOL directly using the
shell, my script runs fine, this only happens in the hol-mode, any clue why
this could happen and how can I fix it?
thanks
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
