From 55ffdf526f8dbf99a88a05910e646446f6bb3421 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 8 Jun 2017 13:08:13 -0400
Subject: Mirror dpdgraph's travis test more accurately

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

(limited to 'dev/ci')

diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh
index 44b0e4c4d5..e8018158bf 100755
--- a/dev/ci/ci-coq-dpdgraph.sh
+++ b/dev/ci/ci-coq-dpdgraph.sh
@@ -7,4 +7,4 @@ coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph
 
 git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR}
 
-( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && (make tests | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) )
+( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make tests && (make tests | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) )
-- 
cgit v1.2.3