aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.ci
diff options
context:
space:
mode:
authorGravatar Beta Ziliani <bziliani@famaf.unc.edu.ar>2018-04-25 14:17:51 -0300
committerGravatar Beta Ziliani <bziliani@famaf.unc.edu.ar>2018-04-25 15:22:57 -0300
commitf725580ecffa96cb0bfd526737586f7a36499286 (patch)
tree29e98ebd4336ad53e46388efac4f868e956771cb /Makefile.ci
parent6d4d16eb5518a9fb461e0f0433c9ce54d2197158 (diff)
updating CI for Mtac2
Diffstat (limited to 'Makefile.ci')
-rw-r--r--Makefile.ci2
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 \