>>>>> On Tue, 25 Dec 2001 21:31:25 +0100, Albrecht Frank <abfrankffm at web.de> said:
> Sorry, not yet. But it can be fixed easily. Perhaps you'd been a
> 'bit hasty' and you forgot to delete the line you wanted to
> replace? ;-)
Uuuups. You're right. But now it's fixed and in CVS.
--
Thomas