From f5adde067368cd6d0b3470be1253cb3629bad2c1 Mon Sep 17 00:00:00 2001 From: Gaƫtan Gilbert Date: Wed, 13 Dec 2017 16:49:26 +0100 Subject: Circle CI: cat failed test suite logs --- test-suite/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/Makefile') diff --git a/test-suite/Makefile b/test-suite/Makefile index 6865dcc76..dbd63a57b 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -177,7 +177,7 @@ summary.log: report: summary.log $(HIDE)bash save-logs.sh $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi - $(HIDE)if [ -n "${APPVEYOR}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi + $(HIDE)if [ "(" -n "${APPVEYOR}" ")" -o "(" -n "${CIRCLECI}" ")" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### -- cgit v1.2.3