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, 3 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1814aaff1..1742660c8 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -314,6 +314,9 @@ ci-hott:
ci-iris-lambda-rust:
<<: *ci-template
+ci-ltac2:
+ <<: *ci-template
+
ci-math-classes:
<<: *ci-template