diff options
| -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 |