From 1533877886e865ff57aa4946d9536871c8df5f3e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 3 Dec 2024 16:55:36 +0100 Subject: [PATCH] Change CI tags to use Coq's runners in addition to shared runners --- .gitlab-ci.yml | 3 --- 1 file changed, 3 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 4431dbd66d..b458a4908e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -33,7 +33,6 @@ before_script: .opam-build: stage: build tags: - - ci.inria.fr - medium script: | PR=${CI_COMMIT_REF_NAME##pr-}; @@ -52,7 +51,6 @@ before_script: json-data: stage: build tags: - - ci.inria.fr - medium variables: COMPILER: "4.11.2" @@ -73,7 +71,6 @@ json-data: opam-lint: stage: lint tags: - - ci.inria.fr - medium variables: COMPILER: "4.11.2"