FYI, I've pushed this. Andrew, I had been playing with git commit --amend --date, and reset the author of patch 1 to me by mistake. I only noticed it too late, after pushing... sorry. -- Pedro Alves