Git cheatsheet and helpful commands

Cheatsheets

https://services.github.com/on-demand/downloads/github-git-cheat-sheet.pdf

The usual pipelines

• Clone a repository

git clone https://github.com/inria-larsen/icub-manual/wiki

• Pulling updates

git pull

• Checking local modifications

git status

• How to push a local modification

    git add <name_of_files>
    git commit -m "message" 
    git pull
    git push

Tricks and configs

• How to check the current URL of your repository:

git remote -v

• How to change the URL of the repository:

git remote set-url origin https://github.com/inria-larsen/robots-configuration.git

This is very useful if you are on a shared machine and you want to avoid people pushing with a common ssh key. In that case, you will have to enter your credentials (login/password) to push.

• How to change the default text editor when comments are merged:

git config --global core.editor "gedit"