>>>>> "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
>>>>> "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