diff --git a/Jenkinsfile b/Jenkinsfile index 31fe4bc4db277167fe18a484a05cdc7ce325e0fc..5f5adb03f01dd292cf688706bfa76b12d71ea278 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -108,6 +108,7 @@ pipeline { '-DOGS_BUILD_TESTS=OFF ' } build { } + build { target="doc" } } } post { @@ -115,6 +116,7 @@ pipeline { publishReports { } } success { + dir('build/docs') { stash(name: 'doxygen') } script { step([$class: 'WarningsPublisher', canResolveRelativePaths: false, messagesPattern: """