From 928bced545407a2043fe2acaa5b31b1aa07988d5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 7 May 2019 14:43:55 +0200
Subject: Remove ppedrot/ltac2 from CI after integration in main repo

---
 Makefile.ci | 1 -
 1 file changed, 1 deletion(-)

(limited to 'Makefile.ci')

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 \
-- 
cgit v1.2.3