Hi,
after talking to our infra guys and alexxy about it, I came to the point
that we should still allow commits to both repos for everyone with
commit access.
To avoid future trouble here are some rules to stick to.
* Don't _amend_ already pushed commits.
* Don't _rebase_ already pushed commits.
* Don't --force a push.
In case you still have problems, then follow this receipt from alexxy.
He will write some longer instructions soonish in the wiki.
$ git fetch --all (assume that you added github as another upstream.
origin is g.o.g.o and github is github)
$ git merge github/master
$ git push origin
that will merge github to g.o.g.o
now we should merge g.o.g.o back to github
$ git checkout -b github github/master
$ git merge origin/master
$ git push github HEAD:master
$ git checkout master
That should fix our problems.
Justin