Introduce tags for Inria GitLab CI.

coq · Oct 16, 2024 · 0b76465 · 0b76465
1 parent ad48495
commit 0b76465
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -32,6 +32,9 @@ before_script:
 
 .opam-build:
   stage: build
+  tags:
+    - ci.inria.fr
+    - medium
   script: |
     PR=${CI_COMMIT_REF_NAME##pr-};
     echo "Github PR number: $PR";
@@ -48,6 +51,9 @@ before_script:
 # Json
 json-data:
   stage: build
+  tags:
+    - ci.inria.fr
+    - medium
   variables:
     COMPILER: "4.11.2"
   script: |
@@ -66,6 +72,9 @@ json-data:
 # Lint
 opam-lint:
   stage: lint
+  tags:
+    - ci.inria.fr
+    - medium
   variables:
     COMPILER: "4.11.2"
   script: