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
