diff --git a/Jenkinsfile b/Jenkinsfile index 025f423b2e30987719dfe69d98c930143b5f2e74..eb7c778f7733a035a7c3b5fddb895d36160a3eca 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -110,13 +110,13 @@ pipeline { post { always { publishReports { } + dir('scripts/jenkins') { stash(name: 'known_hosts', includes: 'known_hosts') } + dir('build/docs') { stash(name: 'doxygen') } } failure { dir('build') { deleteDir() } } success { - dir('build/docs') { stash(name: 'doxygen') } - dir('scripts/jenkins') { stash(name: 'known_hosts', includes: 'known_hosts') } script { publishHTML(target: [allowMissing: false, alwaysLinkToLastBuild: true, keepAll: true, reportDir: 'build/docs', reportFiles: 'index.html',