Cloning a project
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, …
Knowing the URL (or path) of a
git repository, the command is the following
❯ git clone path/of/the/repository where/to/store/it
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.
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
It is actually possible for a repository to have multiple remotes. In this case, instead of removing the
origin, we could have juste renamed it. Here is the command line to rename
upstream for example (
origin is generally reserved for the remote on which you have access):
❯ 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)
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.