diff options
| author | Enrico Tassi | 2020-09-11 09:49:04 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-09-11 09:49:04 +0200 |
| commit | 8d17e971db2d29fad93443e730ee378ec768ba68 (patch) | |
| tree | 2bc9f1b941c31dbdffebc57e5422b3bc33c02dca /.gitlab-ci.yml | |
| parent | 39d3e313614d33b353978847f8d00d3fa2f2428f (diff) | |
rm docker run
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3f8309a..eb221d7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -70,7 +70,6 @@ make-coq-latest: script: - docker build --pull --build-arg=coq_image="coqorg/${CI_JOB_NAME//-/:}" --build-arg=compiler="${OPAM_SWITCH}" -t "${IMAGE}" . - docker push "${IMAGE}" - - docker run --mount "type=bind,source=$(pwd),target=/home/coq/mathcomp" -w /home/coq/mathcomp -t "${IMAGE}" /bin/bash --login -c "set -x; cd mathcomp; make test-suite" - docker logout "${CI_REGISTRY}" except: - tags |