diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2017-06-08 13:08:13 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2017-06-08 13:08:13 -0400 |
| commit | 55ffdf526f8dbf99a88a05910e646446f6bb3421 (patch) | |
| tree | 6ca50caa2cbd2e4139fafbace1f7d81339b6d2b3 /dev | |
| parent | 29ba5cdc0ea31ea62c727f8dcf53d2c805d4bcb3 (diff) | |
Mirror dpdgraph's travis test more accurately
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-coq-dpdgraph.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh index 44b0e4c4d..e8018158b 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) ) |