diff options
Diffstat (limited to 'Makefile.ci')
| -rw-r--r-- | Makefile.ci | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Makefile.ci b/Makefile.ci index a244c17ef3..95ebd64ba1 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -32,7 +32,6 @@ CI_TARGETS= \ ci-coqhammer \ ci-hott \ ci-iris-lambda-rust \ - ci-ltac2 \ ci-math-classes \ ci-math-comp \ ci-mtac2 \ |
