From cb2ee2d949899a897022894b750afd1f3d2eb478 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 5 Nov 2018 19:37:11 +0100
Subject: Integrate plugin tutorial after code import

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

(limited to 'Makefile.ci')

diff --git a/Makefile.ci b/Makefile.ci
index 84be169f57..b8bff98f5f 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -36,7 +36,6 @@ CI_TARGETS= \
     ci-math-comp \
     ci-mtac2 \
     ci-paramcoq \
-    ci-plugin_tutorial \
     ci-quickchick \
     ci-relation-algebra \
     ci-sf \
-- 
cgit v1.2.3