Version Control with Git#

Professional software development typically leverages versioning to keep track of changes. Git is a powerful tool to collaborate on sophisticated projects, and GitHub provides a convenient interface.

Background reading#

See: GitHub Hello World

See: GitHub workflow

Git tips#

Fork a repository#

To fork (creating a copy of a repository, that does not belong to you), you simply have to go to the repository’s webpage dashboard and click fork on the upper right corner.

Clone a repository#

To clone a repository, copy either the HTTPS or SSH link from the repository’s webpage. The following command will download the git repository in a new directory on the local computer (starting from the current working directory).

git clone [email protected]:USERNAME/REPOSITORY

If you have SSH setup properly, you can directly download it. If you are using the HTTPS then github will ask for your credentials.

Move between branches#

You can move to a different branch using the command,

git checkout ![destination-branch]

Create a new branch#

After you successfully cloned a repository, you may want to work on your own branch. Move to the branch you want to start from and run the following command,

git checkout -b ![branch-name]

To see which branch you are working on you can either use both of these commands

git branch
git status

The latter provides more information on which files you might have changed, which are staged for a new commit or that you are up-to-date (everything is ok).

Commit and Push changes#

After you edit some files, you want to push your changes from the local to the remote location. Check the changes that need to be committed/pushed with the command,

git status

Use the following command to mark a ![file] as ready to be committed,

git add ![file]

Once you have marked all the files you want to include in the next commit, complete the commit with a commit message to let collaborators know what you have changed,

git commit -m "![commit-message]"

If everything went well, you are now ready to push your changes to your remote with,

git push origin ![branch-name]

Fetch new branches#

If new branches have been pushed recently to the repository and you don’t have them you can invoke a

git fetch --all

to see all new branches and checkout to those.

Delete branches#

To delete a local branch execute (you cannot be on the branch that you are going to delete!):

git branch -d ![branch-name]

To delete a remote branch you need to push the delete command:

git push origin --delete ![branch-name]

Open a pull request#

If you are working on another branch than the master or forked a repository and want to propose changes you made into the master, you can open a so-called pull-request. To do so, press the corresponding tab in the dashboard of a repository and then press the green button New pull request. You will be asked which branch from which fork you want to merge.

Git troubleshooting#

Problem 1: https instead of ssh:#

The symptom is:

$ git push
Username for 'https://github.com':

Diagnosis: the remote is not correct.

If you do git remote you get entries with https::

$ git remote -v
origin  https://github.com/duckietown/Software.git (fetch)
origin  https://github.com/duckietown/Software.git (push)

Expectation:

$ git remote -v
origin  [email protected]:duckietown/Software.git (fetch)
origin  [email protected]:duckietown/Software.git (push)

Solution:

git remote remove origin
git remote add origin [email protected]:duckietown/Software.git

Problem 2: git push complains about upstream#

The symptom is:

fatal: The current branch ![branch name] has no upstream branch.

Solution:

$ git push --set-upstream origin ![branch name]