just a quick note - the git repo is in a weird state atm. I accidentally pushed a change to tp31 thinking i would then instantly merge to tp32/master, but I think marko has a change on tp32 that he hasn't merged to master yet (so he basically did the same thing i did and pushed too early).
So right now, merging is sorta locked up behind marko's merge to master and I need to step away for a few minutes leaving git kinda weird. Typically, the flow for a merge should involve getting the entire situation clear in all branches first before pushing. So if your change is on tp31, then merge it locally to tp32 and then merge tp32 to master locally - resolve conflicts and test as needed. Then when all good, push in reverse order to each of the branches. Using that same example, start with master and then go to tp32 and then tp31. I think that should limit weirdness if someone is pulling while you are pushing. The same logic would apply if you produced multiple pull requests for the same change which may become the norm at some point in the future. Anyway, until we sort out the merge backup, please refrain from merging between branches. I'll be back online shortly.
