aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-01-08 12:11:12 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-01-08 12:11:12 +0100
commit49d4ca23a9d3c61df485d152de734cdc6418d89a (patch)
tree58a9d638894560794b2eb9e0e2ba11076ddb4bde /dev/tools
parenteece27397cb3befe9d4c7cdad65d3a38b61d7a36 (diff)
github-check-prs.py: print PR URLs when needed.
Diffstat (limited to 'dev/tools')
-rwxr-xr-xdev/tools/github-check-prs.py2
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py
index 7c9043e63..beb26d910 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")