>>>>> "Martin" == Martin Vermeer <[EMAIL PROTECTED]> writes:

>>  It was this one. However, I'd propose this one instead.

Martin> Yes, this seems to work just fine. And looks saner.

I committed it.

JMarc

Reply via email to