On 06/03/2013 01:47 AM, Pádraig Brady wrote: > Yes that's a bit better and fits in the line, > so I've pushed that in your name.
Thanks. Usually, we're mentioning the bug in the commit, don't we? Well, this one was reported as a wishlist bug, together with the solution, and it was trivially enough, so I think it's okay. Have a nice day, Berny
