Pushed as commit 50be0da7bfd5c108697679effeb2a893d2f37598, closing.