* gregor herrmann: > I see that you've pushed the tag in the meantime; thanks for that! > > If there's still outstanding cleanup to do, I'd try `git pull > --rebase' but a merge commit is also no problem; just a force push > onto a published repo should be avoided. Alright, I'll do a merge + cleanup then. Thanks for clarifying. Cheers, -Hilko