gitlab-ci: shorten the names of some jobs
We seem to have about 18-20 chars that can be displayed on the job list (and tons of empty space...), so let's try to use shorter names.
Due to an influx of spam, we have had to impose restrictions on new accounts. Please see this wiki page for instructions on how to get full permissions. Sorry for the inconvenience.
We seem to have about 18-20 chars that can be displayed on the job list (and tons of empty space...), so let's try to use shorter names.