| 1 |
On 2013-11-08 09:22, justin wrote: |
| 2 |
> Hi, |
| 3 |
> |
| 4 |
> after talking to our infra guys and alexxy about it, I came to the |
| 5 |
> point |
| 6 |
> that we should still allow commits to both repos for everyone with |
| 7 |
> commit access. |
| 8 |
> |
| 9 |
> To avoid future trouble here are some rules to stick to. |
| 10 |
> |
| 11 |
> * Don't _amend_ already pushed commits. |
| 12 |
> * Don't _rebase_ already pushed commits. |
| 13 |
> * Don't --force a push. |
| 14 |
> |
| 15 |
> In case you still have problems, then follow this receipt from alexxy. |
| 16 |
> He will write some longer instructions soonish in the wiki. |
| 17 |
> |
| 18 |
> $ git fetch --all (assume that you added github as another upstream. |
| 19 |
> origin is g.o.g.o and github is github) |
| 20 |
> $ git merge github/master |
| 21 |
> $ git push origin |
| 22 |
> that will merge github to g.o.g.o |
| 23 |
> now we should merge g.o.g.o back to github |
| 24 |
> $ git checkout -b github github/master |
| 25 |
> $ git merge origin/master |
| 26 |
> $ git push github HEAD:master |
| 27 |
> $ git checkout master |
| 28 |
> |
| 29 |
> That should fix our problems. |
| 30 |
> |
| 31 |
Thank you Justin for taking the lead on that. |
| 32 |
A nice recipe to solve the problem is better than pushing and then |
| 33 |
going "bugger now I will have to wait for someone else to fix it". |
| 34 |
|
| 35 |
Francois |
Archives