diff options
| -rw-r--r-- | .gitlab-ci.yml | 10 | ||||
| -rwxr-xr-x | test-suite/save-logs.sh | 5 |
2 files changed, 12 insertions, 3 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 9ba39abdbd..3b1ea0d1f8 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -100,13 +100,17 @@ before_script: .test-suite-template: &test-suite-template stage: test script: - - set -e - cd test-suite - make clean # careful with the ending / - make -j ${NJOBS} BIN=$(readlink -f ../install/bin)/ LIB=$(readlink -f ../install/lib/coq)/ all - - cat summary.log - - set +e + after_script: + - test-suite/save-logs.sh + artifacts: + name: "$CI_JOB_NAME.logs" + when: on_failure + paths: + - logs .validate-template: &validate-template stage: test diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh new file mode 100755 index 0000000000..131bcf5451 --- /dev/null +++ b/test-suite/save-logs.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash + +WHERE="logs" + +rsync -a --from0 --files-from=<(find . -name '*.log' -print0) . "$WHERE" |