diff --git a/Jenkinsfile b/Jenkinsfile index f983d6c9d..3d493a0e3 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -10,10 +10,12 @@ pipeline { } post { always { - utils = new Utils() - utils.publish_coverage('coverage.xml') - utils.publish_coverage('coverage.xml') - utils.publish_coverage_native('index.html') + script { + utils = new Utils() + utils.publish_coverage('coverage.xml') + utils.publish_coverage_native('index.html') + utils.publish_pylint('pylint.out') + } mergeJunitResults() } }