On 11 Jan 2011, at 12:56, "Raimund Steger" <rs at mytum.de> wrote: > Ah OK, well given that it is not much of a problem in practice, it can > probably stay like that anyway. Please avoid top-posting. And I actually intend to change it, but it won't work as a fix to this issue. >