ci issueshttps://gitlab.rts.mpi-sws.org/iris/ci/-/issues2021-05-20T11:59:17Zhttps://gitlab.rts.mpi-sws.org/iris/ci/-/issues/2Introduce some kind of pre-merge gating on CI2021-05-20T11:59:17ZRalf Jungjung@mpi-sws.orgIntroduce some kind of pre-merge gating on CIIt would be great to adapt the ["not rocket science"](https://graydon2.dreamwidth.org/1597.html) principle for at least some of our repositories. That means that we would set things up such that CI runs *before* anything enters the maste...It would be great to adapt the ["not rocket science"](https://graydon2.dreamwidth.org/1597.html) principle for at least some of our repositories. That means that we would set things up such that CI runs *before* anything enters the master branch.
Right now, on GitLab this requires an external bot, such as [marge-bot](https://github.com/smarkets/marge-bot).