makarius at sketis.net
Sat Sep 22 13:35:53 CEST 2012
This is just a note on the sporadic failures of HOL-Mirabelle-ex we see
recently from isatest. Technically, the ML/bash invocation
I first thought it would be related to the polyml-5.5.0 update, but I've
seen the same with polyml-5.4.1 occasionally.
Maybe it is again some odd boundary cases with signal handlers in perl, on
different platforms and different perl compilations.
This requires further investigation.
More information about the isabelle-dev