diff --git a/Jenkinsfile b/Jenkinsfile index 7ea1c2495..f8dc0882d 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -11,6 +11,12 @@ pipeline { stages { stage('env setup') { steps { + script { + // CHANGE_ID is set only for pull requests, so it is safe to access the pullRequest global variable + if (env.CHANGE_ID) { + currentBuild.displayName = "PR #${pullRequest.number}: ${pullRequest.title}" + } + } sh 'make setup' } }