diff options
| author | Gaëtan Gilbert | 2018-05-11 22:26:04 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-11 22:26:04 +0200 |
| commit | c24fcbe937bcb84d7fd5e441ff6cbbad589fa096 (patch) | |
| tree | b364bc04f7cbdbcd1b88aecfe3532b9b0f4a721a | |
| parent | 7a6cac1942281fbd66c0e46e3be068b9198addce (diff) | |
gitlab CI: remove math-classes job
It's redundant as a dependency of formal-topology.
| -rw-r--r-- | .gitlab-ci.yml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ac4304da13..2f5a000169 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -278,9 +278,6 @@ ci-iris-lambda-rust: ci-ltac2: <<: *ci-template -ci-math-classes: - <<: *ci-template - ci-math-comp: <<: *ci-template-flambda |