Skip to content

add safe dir for build directory

Lennard Gäher requested to merge lennard/opam2-safe-dir into opam2

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.

Merge request reports