build details

Show: section status errors & todos local changes recent changes last change in-page changes feedback controls

Git for development

Modified 2019-09-22 by Andrea Censi

Learn how to use Git and Github.

This guide provides a basic overview on how do version control with Git.

Background reading

Modified 2019-09-22 by Andrea Censi

Pointers to Git and Github guides.

You should read a good book about Git.

We suggest you work through the Github guides, such as:

For the more advanced topics:

And you should know nobody remembers all Git commands:

My first exercise.

Git setup

Modified 2019-09-22 by Andrea Censi

Installation

Modified 2019-09-22 by Andrea Censi

The basic Git program is installed using

$ sudo apt install git

Additional utilities for git are installed using:

$ sudo apt install git-extras

This include the git-ignore utility, which comes in handy when you have files that you don’t actually want to have pushed to the remote branch (such as temporary files).

Setting up global configurations for Git

Modified 2019-09-22 by Andrea Censi

This should be done twice, once on the laptop, and later, on the robot.

These options tell Git who you are:

$ git config --global user.email "email"
$ git config --global user.name  "full name"

Also do this, and it doesn’t matter if you don’t know what it is:

$ git config --global push.default simple

Git terms explained

Modified 2019-09-22 by Andrea Censi

Repository

Modified 2019-09-22 by Andrea Censi

A repo (short for repository), or Git project, encompasses the entire collection of files and folders associated with a project, along with each file’s revision history.

You can see the repositories for the Duckietown project here.

Branch

Modified 2019-09-22 by Andrea Censi

A branch is a version of the main code, that you can work on and it’s changes won’t affect the main code until it is merged into the master branch. When several people collaborate on a project, it makes sense for each developer to work on his own branch.

Fork

Modified 2019-09-22 by Andrea Censi

A fork is basically a copy of someone else’s repository. Usually, you cannot create branches or change code in other people’s repos, thats why you create your own copy of it. This is called forking.

Git basic actions

Modified 2019-09-22 by Andrea Censi

Fork a repository

Modified 2019-09-22 by Andrea Censi

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

Modified 2019-09-22 by Andrea Censi

To clone a repository, either copy the HTTPS or SSH link given on the repository’s webpage. Then invoke following command to download the git repository onto the local computer (actual directory you are in right now).

$ git clone git@github.com:username/repository.git

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

Create a new branch

Modified 2019-09-22 by Andrea Censi

After you successfully cloned a repository, you may want to work on your own branch in order not to cause any chaos in the master branch. It is usually protected against changes. For this, you can branch out from the master or any other branches by invoking the 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

Modified 2019-09-22 by Andrea Censi

After you edited some files, you want to push your changes from the local to the remote location. In order to do so, first do a double-check on which files you have changed and if things look legitimate. Invoke

$ git status

and check the output. There will be several files, that show up in red. These are files you have changed, but not yet added for a future commit. Most of the time you want to push all your changes so you add them to your commit by executing

$ git add --all

If you do not want to add all files, single files can be added. Then you need to specify each single file

$ git add file-path

After you solved this, add a commit message to let collaborators know, what you have changed:

$ git commit -m "commit-message"

If everything went smooth without any issues you are ready to push your changes to your branch:

$ git push origin branch-name

Fetch new branches

Modified 2019-09-22 by Andrea Censi

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

Modified 2019-09-22 by Andrea Censi

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

Modified 2019-09-22 by Andrea Censi

If you are working on another branch than the master or if you forked a repository and want to propose changes you made into the master, you can open a so-called pull-request. In order 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.

Submitting issues

Modified 2019-09-22 by Andrea Censi

If you are experiencing issues with any code or content of a repository (such as this operating manual you are reading right now), you can submit issues. For doing so go to the dashboard of the corresponding repository and press the Issues tab where you can open a new request.

Git advanced tips

Modified 2019-09-22 by Andrea Censi

Delete branches

Modified 2019-09-22 by Andrea Censi

Delete local:

$ git branch -d branch-name

Delete remote:

$ git push origin --delete branch-name

Propagate on other machines by doing:

$ git fetch --all --prune

Shallow clone

Modified 2019-09-22 by Andrea Censi

You can clone without history with the command:

$ git clone --depth 1 repository URL

Git troubleshooting

Modified 2019-09-22 by Andrea Censi

Problem: https instead of ssh

Modified 2019-09-22 by Andrea Censi

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  git@github.com:duckietown/Software.git (fetch)
origin  git@github.com:duckietown/Software.git (push)

Solution:

$ git remote remove origin
$ git remote add origin git@github.com:duckietown/Software.git

Problem: git push complains about upstream

Modified 2019-09-22 by Andrea Censi

The symptom is:

fatal: The current branch branch name has no upstream branch.

You have not associated the current branch to the remote.

Solution:

$ git push --set-upstream origin branch name