More git things

1. Get all the tags (releases most likely) 

     git fetch --all --tags 

2. Then checkout a specific tag

     git checkout tags/1.12.5 -b my1.12.5 

 3. Check you are indeed on the branch

     git branch

 

============

To sync with upstream master branch

1. Fetch upstream branch, for example

    git fetch upstream master

2. Switch to the local branch that you like to sync with the upstream branch

    git rebase upstream/master

 

3. Doing the above may produce conflict, then you will need to resolve the conflicts, then run the following command:

   git rebase --continue

 

4. Most likely you will need to do the following to get your branch pushed to your own remote repo.

   git push -f origin master

============

To get someone else's pull request for build or test purpose, assume that your local repo is the clone of your own repository, and upstream is the upstream repo. then do the following:

1.  git fetch upstream pull/$ID/head:$BRANCHNAME

2. git checkout $BRANCHNAME

Where $ID should be the pull request id which is normally found at the very end of the PR url. $BRANCHNAME should be just a name. Once the fetch command succeeded, you can use git checkout to switch to that branch and do whatever you need to do.