When you have Git repositories as below.
- CENTER.git : Central repository you can not manage
- MAIN.git : Main repository that your team push into
- LOCAL : Local repository on developers local machine
Merge on bare repository
You can't merge on bare repository such as MAIN.git because bare repository has no working copy. There are no ways to resolve the conflict when it occurs. Therefore, you must checkout the target branch into your local repository, merge your commits, then push to bare repository(MAIN.git).
Merge from external repository
Use 'git fetch' when there are some changes on CENTER.git. But this command doesn't update HEAD position. So you should use 'git reset --soft'.
# on MAIN.git $ git fetch <CENTER.git> $ git reset --soft HEADcheck commit histories using 'git log'.
Push specified branch
You can push local branch 'dev-local' into 'dev-remote' on origin.
$ git push origin dev-local:dev-remote
Clone from remote branch
You can checkout 'dev-remote' branch on MAIN.git into 'dev-local' branch on local machine:
git clone <MAIN.git> git checkout -b dev-local remotes/origin/dev-remote
Push tags into remote repository
You can push local tags into remote repository.
$ git push --tags
This article is translated from Japanese.