Hi Tom, FYI I made this local merge but I did not push it, do whatever you like with it. (What I pushed I also reverted and it was not a GIT-merge so it should be a nop.) Jan