diff --git a/dev-support/Jenkinsfile b/dev-support/Jenkinsfile index f1c83083e3e..ce12d9a56a4 100644 --- a/dev-support/Jenkinsfile +++ b/dev-support/Jenkinsfile @@ -480,6 +480,7 @@ curl -L -o personality.sh "${env.PROJECT_PERSONALITY}" echo '(/) {color:green}+1 source release artifact{color}\n-- See build output for details.' >output-srctarball/commentfile else echo '(x) {color:red}-1 source release artifact{color}\n-- See build output for details.' >output-srctarball/commentfile + exit 1 fi """ }