diff options
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index cc8a4d34c9..ca5584bcb5 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -803,7 +803,7 @@ library:ci-geocoq: library:ci-hott: extends: .ci-template -library:ci-lambda_rust: +library:ci-iris: extends: .ci-template-flambda library:ci-math_classes: |