add safe dir for build directory
Since updating the CI image to a current git versions, we are suffering from problems with git's new safe directory feature in the timing runner when pushing the timing information (it takes issue if there is mixed ownership within a checkout). Example of a failing pipeline: https://gitlab.mpi-sws.org/iris/iris/-/jobs/234468
The problem is that the git directory gets cloned by the root
user inside the image, while the ci scripts get run by the ci
user (as declared in the Dockerfile
).
It seems like there is a fix for this on the way in gitlab: https://gitlab.com/gitlab-org/gitlab-runner/-/merge_requests/3538
For now, we can just manually add the /builds
directory as a safe directory.