[ci] Make .gitlab-ci.yml portable

Currently the CI config requires that the core/ci-config project exists on the same gitlab server. This prevents the CI from working when pushing the repository to another server. While one may argue, that one also has to push core/ci-config then, it is a very strong restriction to require that the gitlab group core is available.

This can be avoided by using a gitlab link to the included files directing to the dune server, which still allows to select the master branch.

@simon.praetorius Can you have a look if the proposed change is OK or has any drawbacks?

Maybe we can rewrite the ci-config repo into a CI/CD component provider, https://docs.gitlab.com/ee/ci/components

added 1 commit

• 87b580a9 - [ci] Use 'remote:' for including remote files

Compare with previous version

Could you please do a rebase. The pipeline cannot succeed due to an error in the transposetest

added 9 commits

• 87b580a9...038d9506 - 8 commits from branch master
• 66fec83d - [ci] Make .gitlab-ci.yml portable

Compare with previous version

added 1 commit

• 70bcdbdf - [ci] Make .gitlab-ci.yml portable

Compare with previous version

resolved all threads

resolved all threads

merged

mentioned in commit 6e3484eb