1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.ci b/Makefile.ci
index 6b30f8723..37b14ed91 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -28,7 +28,7 @@ CI_TARGETS=ci-bignums \
     ci-ltac2 \
     ci-math-classes \
     ci-math-comp \
-    ci-metacoq \
+    ci-mtac2 \
     ci-sf \
     ci-tlc \
     ci-unimath \