aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-10 02:56:37 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-10 09:50:06 -0400
commit5b6aaca42550715300fbd376c2fc0934da554939 (patch)
tree438dd5ff004e00e52195f3b13806b4a329990d62 /test-suite
parenta8381e022cf2a967c7c213ec60c5c5252c799332 (diff)
Fix Travis sectioning
It drops anything after a `/`, so we change all `/`s into `.`. There must be a better way to do this that doesn't involve so much bash hackery, right?
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 81a99cad4..5ab4cacda 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -169,7 +169,7 @@ summary.log:
# local build, and downloadable on GitLab)
report: summary.log
$(HIDE)./save-logs.sh
- $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec echo 'travis_fold:start:coq.logs.{}' ';' -exec cat '{}' ';' -exec 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
#######################################################################