Pushed to master as commit 648ae62112f62bc2106fb36d45c83fda787d3bed.