Pushed as 8d27fe61d7f1a2bed0367fa861e4cae1f2f1546d to master.