From 0795fc9118e1d277bdfb1d512a4c17c803152aea Mon Sep 17 00:00:00 2001
From: Michael Kirk <michael@signal.org>
Date: Thu, 10 Jan 2019 13:49:07 -0700
Subject: [PATCH] ci labels PRs with GH title

---
 Jenkinsfile | 6 ++++++
 1 file changed, 6 insertions(+)

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'
             }
         }