Thanks for the recipe!
On Thu, Nov 7, 2013 at 1:22 PM, justin <[email protected]> wrote: > 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 > >
