From 5610d73c418de33b2248eb08074fd2de0383f596 Mon Sep 17 00:00:00 2001
From: Leonidas Lampropoulos <lemonidas_13@hotmail.com>
Date: Thu, 31 May 2018 10:39:47 -0400
Subject: QuickChick CI

---
 Makefile.ci | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Makefile.ci')

diff --git a/Makefile.ci b/Makefile.ci
index ce725d19d..7f63157fa 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -17,6 +17,7 @@ CI_TARGETS=ci-bignums \
     ci-cpdt \
     ci-cross-crypto \
     ci-elpi \
+    ci-ext-lib \
     ci-equations \
     ci-fcsl-pcm \
     ci-fiat-crypto \
@@ -31,6 +32,7 @@ CI_TARGETS=ci-bignums \
     ci-math-comp \
     ci-mtac2 \
     ci-pidetop \
+    ci-quickchick \
     ci-sf \
     ci-tlc \
     ci-unimath \
@@ -50,6 +52,8 @@ ci-math-classes: ci-bignums
 
 ci-corn: ci-math-classes
 
+ci-quickchick: ci-ext-lib
+
 ci-formal-topology: ci-corn
 
 # Generic rule, we use make to ease travis integration with mixed rules
-- 
cgit v1.2.3