diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-13 10:32:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-13 10:32:57 +0200 |
| commit | 5b932123c05c6ef75333dec4d5b91cce403e935e (patch) | |
| tree | a7b0fa9fc82ffcf43e064b790b7b04a2389ae132 /test-suite | |
| parent | 423d3202fa0f244db36a0b1b45edfa61829201e6 (diff) | |
| parent | 5b6aaca42550715300fbd376c2fc0934da554939 (diff) | |
Merge PR#757: Better sectioning on travis log printing in test-suite
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index e15094ccf..5ab4cacda 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -169,9 +169,7 @@ summary.log: # local build, and downloadable on GitLab) report: summary.log $(HIDE)./save-logs.sh - $(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:start:coq.logs'; fi - $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec cat '{}' ';'; fi - $(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:end:coq.logs'; fi + $(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 grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### |