WARNING! Gitlab maintenance operation scheduled for Saturday 28th March from 8 a.m. (CET) to approximately 3 p.m. (CET). GitLab will be unavailable during this time.
This reverts commit a60bde79 I have pushed by mistake. Apologies for my incompetent use of the git repo!