aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml3
1 files changed, 0 insertions, 3 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index bd400f65b..095099690 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -306,9 +306,6 @@ ci-iris-lambda-rust:
ci-ltac2:
<<: *ci-template
-ci-math-classes:
- <<: *ci-template
-
ci-math-comp:
<<: *ci-template-flambda