aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coq-makefile/mlpack2
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-07-17 10:50:04 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-07-20 15:40:48 +0200
commit7f7075d10780fe24c97e329868a501c2af422625 (patch)
tree59666791550e3114c9b8b40cfdf909c71175197b /test-suite/coq-makefile/mlpack2
parentda2d3108f126b3ff7bface118319bfa43829a895 (diff)
coq-makefile: make test suite detect more errors
Replacing ; with && and enabling bash's pipefail option
Diffstat (limited to 'test-suite/coq-makefile/mlpack2')
-rwxr-xr-xtest-suite/coq-makefile/mlpack2/run.sh5
1 files changed, 1 insertions, 4 deletions
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
index 10a200dde..1ca69bf23 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -1,8 +1,5 @@
#!/usr/bin/env bash
-#set -x
-set -e
-
. ../template/init.sh
coq_makefile -f _CoqProject -o Makefile
@@ -10,7 +7,7 @@ make
make html mlihtml
make install DSTROOT="$PWD/tmp"
#make debug
-(cd `find tmp -name user-contrib`; find .) | sort > actual
+(cd `find tmp -name user-contrib` && find .) | sort > actual
sort > desired <<EOT
.
./test