Patch pushed as 8c303758590e368fc6a67bfff8dd1721e70afd93.
I just slightly modified the commit message.
Thanks.