diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b8f31d6c852bc3d5a8daff89a10a44b6b76be06f..907e4ae53fb397477ea2bbe6d67a615e3ae69f4e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -5,13 +5,13 @@ stages: variables: CPU_CORES: "10" - GIT_SUBMODULE_STRATEGY: "recursive" .template: &template stage: build tags: - fp script: + - git clone https://gitlab.mpi-sws.org/FP/iris-ci.git ci -b opam2 - ci/buildjob cache: key: "$CI_JOB_NAME" diff --git a/ci b/ci deleted file mode 160000 index c3b53061d2452f7ea50766915eb40312163d155a..0000000000000000000000000000000000000000 --- a/ci +++ /dev/null @@ -1 +0,0 @@ -Subproject commit c3b53061d2452f7ea50766915eb40312163d155a