Eildert Groeneveld wrote: > Dear all > it seems that the problem reported below has disappeared after the last CVS > updates. Sometimes really starnge things happen. Like, developers fixing a bug? :-) As I wrote earlier, thank you for pointing out this bug, and I fixed it last weekend. It wasn't anything "strange" -- it was perfectly valid to report this bug, so that we can work on it. Christian