Our CI vs. GitLab CI
$ADMIN is considering deprecating our self-hosted CI server
in favor of GitLab CI because the CI server uses 80.8MB (~16%)
of our (precious) RAM (in idle mode!). (And GitLab CI is probably technically
superior than the service we are hosting.)
To make a possible migration easier, here is already a tutorial-like wiki page describing how to use GitLab CI for LaTeX projects.