Patch pushed as df898f7206f3925cdc041a8578d9dbff2f0118f1. Thanks.