[isabelle-dev] HOL-Mirabelle-ex

[Makarius]

This is just a note on the sporadic failures of HOL-Mirabelle-ex we see 
recently from isatest. Technically, the ML/bash invocation 
http://isabelle.in.tum.de/repos/isabelle/file/355f3d076924/src/HOL/Mirabelle/ex/Ex.thy#l5 
somehow "hangs".

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.


 	Makarius