From 4aae5846dbe685a0e99e296053b57345b11c4330 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 6 Jun 2017 14:27:01 -0400
Subject: [travis] Also run coqchk on HoTT

---
 dev/ci/ci-hott.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 6ded97984e..184b90a50b 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -7,4 +7,4 @@ HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT
 
 git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}"
 
-( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make )
+( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make && make validate )
-- 
cgit v1.2.3