Moritz, thanks for the text. There is still some discussion about how to handle #502140. Do you think, we should add your text anyway? (And we should add a link to that bug, right?)
-- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]