diff --git a/_assets/ci/Jenkinsfile.tests b/_assets/ci/Jenkinsfile.tests index bf4ff02fd..8bbad5925 100644 --- a/_assets/ci/Jenkinsfile.tests +++ b/_assets/ci/Jenkinsfile.tests @@ -175,7 +175,12 @@ pipeline { } } success { script { github.notifyPR(true) } } - failure { script { github.notifyPR(false) } } + failure { + script { + github.notifyPR(false) + archiveArtifacts('**/test_*.log') + } + } cleanup { dir(env.TMPDIR) { deleteDir() } sh "make git-clean"