diff options
| author | Erik Martin-Dorel | 2018-12-20 16:18:28 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2018-12-21 12:17:07 +0100 |
| commit | da5985eae6656be1bd30aee76c8d08dbc3a09c25 (patch) | |
| tree | 5574ca1c18e076a672da3a26672dccfcecd465ae /.gitlab-ci.yml | |
| parent | 1c14614a2328d1854fd584d8d7ca54121faec0ee (diff) | |
chore: s/.build/.opam-build/
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 574a3b2..6c70f50 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -28,7 +28,7 @@ stages: - test # set var OPAM_SWITCH (if need be) when using -.build: +.opam-build: stage: build image: docker:latest services: @@ -57,18 +57,18 @@ stages: - merge_requests coq-8.6: - extends: .build + extends: .opam-build variables: OPAM_SWITCH: "base" coq-8.7: - extends: .build + extends: .opam-build coq-8.8: - extends: .build + extends: .opam-build coq-dev: - extends: .build + extends: .opam-build # set CONTRIB_URL, script, COQ_VERSION, CONTRIB_VERSION when using .ci: |