From 2948f2b8afd4110c59eba6af05ff22592e49501c Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 20 May 2021 14:23:19 +0200 Subject: [PATCH] separate Coq 8.13 MR job from main job --- .gitlab-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 101c6c57..894fcc50 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -59,7 +59,7 @@ build-coq.8.13.2: - fp-timing # Separate MR job that does not run on fp-timing. -build-coq.8.13.2: +build-coq.8.13.2-mr: <<: *template <<: *only_mr variables: -- GitLab