diff --git a/Jenkinsfile b/Jenkinsfile index 7cb901f663..dfa83fc592 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -157,6 +157,7 @@ pipeline { sh''' git log -1 --pretty=%B | fgrep -ie '[skip ci]' -e '[ci skip] ''' + currentBuild.getRawBuild().getExecutor().interrupt(Result.SUCCESS) } }