From 5648ea629bb269d2204d47b5c6a97c7ecc798724 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 27 Sep 2017 16:52:25 +0200 Subject: [PATCH] rename CI jobs --- .gitlab-ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e2fd9f24..82d07363 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -23,13 +23,13 @@ variables: - master - /^ci/ -lrust-coq8.7: +build-coq8.7: <<: *template variables: COQ_VERSION: "8.7.dev" SSR_VERSION: "dev" -lrust-coq8.6.1: +build-coq8.6.1: <<: *template variables: COQ_VERSION: "8.6.1" -- GitLab