diff options
Diffstat (limited to 'test-suite')
| -rwxr-xr-x | test-suite/report.sh | 16 |
1 files changed, 3 insertions, 13 deletions
diff --git a/test-suite/report.sh b/test-suite/report.sh index cef615266b..71aac029ea 100755 --- a/test-suite/report.sh +++ b/test-suite/report.sh @@ -24,21 +24,11 @@ cp summary.log "$SAVEDIR"/ rm "$FAILED" # print info -if [ -n "$TRAVIS" ] || [ -n "$APPVEYOR" ] || [ -n "$PRINT_LOGS" ]; then +if [ -n "$APPVEYOR" ] || [ -n "$PRINT_LOGS" ]; then find logs/ -name '*.log' -not -name 'summary.log' -print0 | while IFS= read -r -d '' file; do - if [ -n "$TRAVIS" ]; then - # ${foo////.} replaces every / by . in $foo - printf 'travis_fold:start:coq.logs.%s\n' "${file////.}"; - else printf '%s\n' "$file" - fi - + printf '%s\n' "$file" cat "$file" - - if [ -n "$TRAVIS" ]; then - # ${foo////.} replaces every / by . in $foo - printf 'travis_fold:end:coq.logs.%s\n' "${file////.}"; - else printf '\n' - fi + printf '\n' done printed_logs=1 fi |