Pushed as c072887bb0b37aea36d6ba6e0dc636858b4b440a with a few little
fixes. Thanks.