From 57a56d4cfd25cbb4a64f0d1d4b5cc59d55f55778 Mon Sep 17 00:00:00 2001
From: Victor Martinez <victormartinezrubio@gmail.com>
Date: Tue, 28 Apr 2020 17:32:33 +0100
Subject: [PATCH] ci: comment PRs with the build status (#17971) (#18053)

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

diff --git a/Jenkinsfile b/Jenkinsfile
index 1086f730ea72..376be7096ce7 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -580,6 +580,11 @@ pipeline {
       }
     }
   }
+  post {
+    cleanup {
+      notifyBuildResult(prComment: true)
+    }
+  }
 }
 
 def makeTarget(String context, String target, boolean clean = true) {