git repositories on my server

Hi:3

Git is free software and a version control system. We can use it to work together on program code in our exercice groups.

Set up (on Linux)

First, create private and public key

ssh-keygen -t rsa

Save it for examle as ~/.ssh/your_name . You will be asked for a passphrase. Then, send me the public key (the one with .pub) per mail to stern [at] kelvinwaterdropper.org. Note that you have to enable "show hidden files" becaurse .ssh is a hidden directory. I will give you access to the repository. After that, you can clone the repository:

git clone git@kelvinwaterdropper.org:name_of_repository

name_of_repository is machinelearning, 3dreconstruction or simulationmethods.

It asks you for your key passphrase (not for password of git- if this happens, something goes wrong). Now, you should see the repository. If you have other ssh-keys on your laptop, this sometimes does not work and you have to edit ~/.ssh/config and add host and key there.

When you use git for the first time, git wants to know your name and mail adress (they do not have to be correct).

git config --global user.name "your name"

git config --global user.email "youremail@example.com"

How to use

Every time before you start working, pull the repository from the server. cd to the git repository and type:

git pull

Now, you can start programming:)

From time to time, push your changes to the server: Save your file (and maybe shut down the jupyter notebook) and type:

git add name_of_changed_file

git commit -m "comment on what I changed"

git push

Since my server has only 10GB storage (may become more in the future), please save big datasets etc. localy on your laptop and do not add them to the git repository. About 20MB per exercice sheet would be great, with source code alone this should be no problem.

Sometimes, if others changed the same part of the file the same time as you did, there are merge conflicts when you try to push your changes. git provides tools to solve this problems. If git argues about that, first do git pull:

git pull

Using git diff, you can see the differences. Then, open the file that is different. You should see the different lines of both versions. Delete everything you do not want in the file. Save the file and do git add, git commit and git push again. It should work now.