> Fine.  I've pushed your changes now as commit
> e0de9f3295b4c46cb7198ec0b9634809d7b7a36d.  Please have a look and close
> the bug if everything is OK.


Looks good to me except the NEWS entry which on second look wasn't 
precise enough. I have attached a patch which aims to fix it. Thanks for 
all your help!