Gitlab@FMF
Bad news
The old git.fmf.uni-lj.si
ran outdated software (Gitlab version 5.2.0, the
latest version is at 10.x) on an outdated Debian system , running on a virtual
machine with an outdated license. When it crashed, we managed to restore the
virtual machine, but it proved impossible to upgrade Gitlab.
We apologize for the inconvenience.
Good news
We set up a modern Gitlab server which will be more easily maintained in the future.
How to use the new server
Unfortunately, we did not manage to migrate the data from the old server. The
git repositories are still there, somewhere, so if you absolutely need something
from it, Andrej Bauer can dig it out for you. However, in most cases you can
just use the repositories that you have on your local disk. They can be
transferred back to git.fmf.uni-lj.si
, with complete history.
Step 1: create an account on the new server
You can create an account by logging into the server using one of the following options:
-
Local users from the Faculty of mathematics and physics can use the LDAP login method. Use the username
Name.Surname@fmf.uni-lj.si
and the usual departmental password. -
External users can login with a Gmail account.
Step 2: Install SSH credentials
Once you have logged in, you should install your public SSH key.
In your user settings, click on the SSH Keys and add your public SSH key. On
Linux and MacOS you can typically find the key in the file ~/.ssh/id_rsa.pub
.
Step 3: transfer your repositories back to the server
Suppose you have a repository my-repo
on your local disk that you would like
to transfer to the new server. Follow these steps:
-
Create a new project by clicking on the green New button under Projects. It is probably a good idea to keep the same repository name, say
my-repo
. Do not initialize the repository with aREADME
file. -
Follow the instructions for pushing an existing repository at the bottom of the page that you get after creation. They go somewhat like this:
cd my-repo git remote rename origin old-origin git remote add origin ⟨repository-location⟩ git push -u origin --all git push -u origin --tags
Step 3: Give collaborators access to your repository
You can give other users access to the repository, but they need to log into the server at least once first. Use the Members section under the repository Settings. You should give them the Developer or Maintainer status. (If they cannot push, elevate them to Manager, or check whether you have any protected branches under project Settings → Repository → Protected branches.)
Once they have the access, they should clone the repository and dismiss the old one that they have lying around. If they know what they are doing, they may also change the origin
.