Apologies for the messy merge of my branch. One learns all the time. I tried merging the branch locally instead of using the pull request web interface. One has to be careful with every commit - even to a local branch - or just copy files between the branches and commit without a proper merge... /O