From 49d4ca23a9d3c61df485d152de734cdc6418d89a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 8 Jan 2018 12:11:12 +0100
Subject: github-check-prs.py: print PR URLs when needed.

---
 dev/tools/github-check-prs.py | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev/tools')

diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py
index 7c9043e63a..beb26d9104 100755
--- a/dev/tools/github-check-prs.py
+++ b/dev/tools/github-check-prs.py
@@ -38,8 +38,10 @@ for pull in repo.get_pulls():
             labelled = True
     if labelled and not dirty:
         print ("PR #" + str(pull.number) + " is not dirty but is labelled")
+        print ("("+ pull.html_url +")")
     elif dirty and not labelled:
         print ("PR #" + str(pull.number) + " is dirty and not labelled")
+        print ("("+ pull.html_url +")")
     else:
         # give some feedback so the user can see we didn't crash
         print ("PR #" + str(pull.number) + " OK")
-- 
cgit v1.2.3