Tutorial Git

Add ssh key

First thing to do is to add a ssh key to your profile if not already done.

Clone the project

In the following, PROJECT_DIR is a variable standing for the project root directory where the git repositories are stored. For example,

export PROJECT_DIR=${HOME}/my_project_root_directory.

Once you have added a ssh key, you can clone it in a local directory:

cd $PROJECT_DIR
git clone git@gitlab.com:toc-sp/num-comp.git

Git workflow (basic)

We follow the Centralized Workflow. It is basic since we work in the master branch.

Create new files

Update your local repository

cd $PROJECT_DIR
git pull

Then, we assume that you create two files myfile1.txt and myfile2.txt as you want.

Add the two files and update the remote repository

We assume that the files myfile1.txt and myfile2.txt have been created/modified in the $PROJECT_DIR directory and that you want to update the remote repository such that every one can see you changes.

• Add the files

git status
git add myfile1.txt
git add myfile2.txt

Remark. Do not use git add *, but add only the files that must be shared.

• Commit the changes

git commit -m "my message for the commit"

• Update the remote repository, such that every one can see the changes

git push

Handle conflicts

General case

If the local repository has diverged from the remote one, then the push will fail and Git refuse the request with an error mesage:

error: failed to push some refs to '/path/to/repo.git'
hint: Updates were rejected because the tip of your current branch is behind
hint: its remote counterpart. Merge the remote changes (e.g. 'git pull')
hint: before pushing again.
hint: See the 'Note about fast-forwards' in 'git push --help' for details.

This prevents from overwriting official commits. To solve the conflicts, the idea is to pull remote udpates into your local repository, integrate them with your local changes and then try again to push.

• pull to incorporate upstream changes:

git pull

• See the conflicted files

git status

• Edit the conflicted files

Remark. you can choose your local version by

git checkout --ours path/to/file

or the remote version by

git checkout --theirs path/to/file

• Take into account the resolution, that is stage the files

git add <some-file>

• When all the conflicts are solved, then you can commit and update the remote repository:

git commit -m "merged done"
git push

Both added file

If a file myfile.pdf has been added by two persons, you can see:

Unmerged paths:
   (use "git reset HEAD <file>..." to unstage)
   (use "git add/rm <file>..." as appropriate to mark resolution)

       both added:         myfile.pdf

Either you can choose your version by

git add myfile.pdf

or the version already pushed by

git reset HEAD myfile.pdf

then commit and push when your conflicts are solved. Note that you can also remove it for all by

git rm myfile.pdf