improve jenkins #11

Merged
bquarkz merged 2 commits from dev/improve-jenkins into master 2026-04-08 08:24:16 +00:00
Showing only changes of commit a4b0006745 - Show all commits

View File

@ -2,6 +2,9 @@ pipeline {
agent any
environment {
CARGO_HOME = '/var/jenkins_home/.cargo'
CARGO_TARGET_DIR = 'target'
CARGO_TERM_COLOR = 'always'
MIN_LINES = '60'
@ -12,7 +15,6 @@ pipeline {
stages {
stage('Build') {
steps {
script {
sh '''
set -eux
make ci cobertura
@ -50,7 +52,6 @@ pipeline {
echo "Coverage gate passed."
'''
}
// withChecks(name: 'Test', includeStage: true) {
// sh '''
// set -eux
@ -77,7 +78,6 @@ pipeline {
stage('Reports') {
steps {
script {
publishHTML(target: [
allowMissing: false,
alwaysLinkToLastBuild: true,
@ -87,7 +87,8 @@ pipeline {
reportName: 'Rust Coverage HTML',
reportTitles: 'Coverage Report'
])
}
archiveArtifacts artifacts: 'target/llvm-cov/**', fingerprint: true
}
} // Reports
}