Re: To Thomas Munro
> 603 iterations later it hit again, but didn't log anything. (I believe
> I did run "make" in the right directory.)
Since that didn't seem right I'm running the tests again. There are
XXX lines in the output, but it hasn't hit yet.
Christoph