Cloning a project

Using git locally is great. Coupling it with a remote server is better (and simple):

• Even if it is not a backup server, it can be use somehow as a backup
• Access your source code from whenever
• Share it with colleagues, friends, …

Clone

Knowing the URL (or path) of a git repository, the command is the following

❯ git clone path/of/the/repository where/to/store/it

The where/to/store/it is optinal, when not specified, git will create a folder of the same name as the reposity.

How to get the URL of a project online? On the most popular git server (Gitlab, Github, Bitbucket), a link is provided on a repository, as shown on the picture below:

SSH or HTTPS? If you have saved your SSH key on your Gitlab account then you should use SSH otherwise you must use HTTPS. SSH is more secure and do not ask for your password and login every time you git push to the server - if you have to do it. In any case, the remote (protocole and/or URL) can be changed later.

Remote

Information

You can ask git what are the different remote and their path:

❯ git remote -v
origin	https://plmlab.math.cnrs.fr/infomath/git_dummy (fetch)
origin	https://plmlab.math.cnrs.fr/infomath/git_dummy (push)

When cloning a repository, a new remote is created and named origin. A repository can have multiple remotes, but it might be tricky to synchronize them if your aim is to use git as a backup system (which is not!).

Remark that you have access to the complete history of the repository (so be careful of what you commit! git never forget!):

❯ git log
commit c3ee9bbe4f195806f4bc5050f78ff9d4dd70f05c (HEAD -> master, origin/master)
Author: B***d T***y <b***y@***.***.fr>
Date:   Wed Nov 20 15:37:05 2019 +0100

    last commit was a mistake

commit a97f1b2abc0850f7053461258401fe4736e17f4b
Author: B***d T***y <b***y@***.***.fr>
Date:   Wed Nov 20 15:34:10 2019 +0100

    changing title

Deleting a remote

We now want to store our git repository in our git server. The actual remote, origin, is targetting infomath’s repository. We want to remove it as this is not your server:

❯ git remote remove origin
❯ git remote -v

❯ git remote rename origin upstream
❯ git remote -v
upstream	https://plmlab.math.cnrs.fr/infomath/git_dummy (fetch)
upstream	https://plmlab.math.cnrs.fr/infomath/git_dummy (push)

Your server

On your git server (Gitlab, …), create a blank project as follows

Then add it as a remote. Copy the git url of this new (and blank) project, and in your thesis folder, adapt and type the following (either https or ssh!)

❯ git remote add origin https://plmlab.math.cnrs.fr/username/projectname
❯ git push origin

You might need to use the command git push --set-upstream origin for the first push, after that you do not need it anymore. You can now refresh your browser to see the change in the remote server.