Hi all, so we tried a lot of different things ... in the end we deleted gitbox and re-clonned from github as infra didn't have any more clues as to what was causing the problems. Now things should work again ... so feel free to push and from now on it shouldn't matter if you push to github or gitbox and merging PRs in the GitHub web-ui should be fine also.
Now I have to finish some not quite working stuff in the cpp maven build as I had to comit something that wasn't done to produce a new PR ;-) So all keep your fingers crossed and: https://www.youtube.com/watch?v=vCadcBR95oU Chris Am 22.03.19, 08:47 schrieb "Christofer Dutz" <[email protected]>: We're working with infra to get the sync work in the direction from GitHub ... So please don't do any commits and especially no pushing for now. I'll inform you as soon as we can continue. https://issues.apache.org/jira/plugins/servlet/mobile#issue/INFRA-18056 Chris Outlook für Android<https://aka.ms/ghei36> herunterladen
