Merge PR #9383: Remove travis

Reviewed-by: Zimmi48
Reviewed-by: vbgl

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