diff --git a/Jenkinsfile b/Jenkinsfile index 9c5ea9228f..c351f8e032 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -15,7 +15,7 @@ pipeline { } stage('Build') { steps { - sh 'ninja 2>&1 | tee build_log.txt' + sh "bash -o pipefail -c 'ninja 2>&1 | tee build_log.txt'" } } stage("Comment") {