Pushed to master as commit ef6d3b643689953b71fe103e8c6f520b54996f11, closing.