On Sat, 18 Sep 2004 21:08:20 +0200 Reimar Döffinger <Reimar.Doeffinger at stud.uni-karlsruhe.de> wrote: > does that still happen with current CVS? I did a cvs-up and the problem is gone now. Of course, with my luck, I'll probably find another bug in the next few minutes...