From 409da1f63e685e9af39a54da61ab655f2c345b00 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 11 Aug 2022 11:27:00 -0400 Subject: [PATCH] don't do dev test in MRs --- .gitlab-ci.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 2e88890b..89a6285e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -44,7 +44,6 @@ variables: build-coq.8.16.dev: <<: *template - <<: *branches_and_mr variables: OPAM_PINS: "coq version 8.16+rc1" -- GitLab