From b83ee9bf7dea03a211a0630b2bd5d08ad885cad8 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 27 Jun 2017 14:54:57 -0400
Subject: Have coq-dpdgraph ci test print the differences

This allows better debugging when it fails.
---
 dev/ci/ci-coq-dpdgraph.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh
index e8018158bf..b610f70004 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 && (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 test-suite )
-- 
cgit v1.2.3