Hi Michael,

Your patch looks good!  It has been pushed to master as commit d33b7a2f.

Thanks,
Kei