Jan> FYI I made this local merge but I did not push it, do whatever you Jan> like with it. Jan> (What I pushed I also reverted and it was not a GIT-merge so it should be Jan> a nop.) Thanks. I actually had already done a rebase here, but I did it late on Friday and then didn't think to push it. Sorry about the duplicated work. Tom