My patch needed rebasing before commit. This is the danger of the github web push interface which doesn't do a new build close to ToT.
