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:

1. 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 a README file.

2. 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.