diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-28 21:39:36 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-30 20:09:38 +0100 |
commit | 98eb51ae14eeb281648fef6f02f98a333cef382b (patch) | |
tree | d2283d5ac9979c4da1adb3dffa500e0987cd7121 /dev | |
parent | 7e319ad03aba413f3165b848eaf821b364f9291b (diff) |
Python script checking missing/unnecessary [needs: rebase] label
Diffstat (limited to 'dev')
-rwxr-xr-x | dev/tools/github-check-prs.py | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py new file mode 100755 index 000000000..2ba751d07 --- /dev/null +++ b/dev/tools/github-check-prs.py @@ -0,0 +1,29 @@ +#!/usr/bin/env python3 + +# Requires PyGithub https://pypi.python.org/pypi/PyGithub +from github import Github + +REPO = "coq/coq" +REBASE_LABEL="needs: rebase" + +token = input("Github access token: ") + +g = Github(token) + +repo = g.get_repo(REPO) + +for pull in repo.get_pulls(): + # if conflicts then dirty + # otherwise blocked (because I have no rights) + dirty = pull.mergeable_state == "dirty" + labelled = False + for label in repo.get_issue(pull.number).get_labels(): + if label.name == REBASE_LABEL: + labelled = True + if labelled and not dirty: + print ("PR #" + str(pull.number) + " is not dirty but is labelled") + elif dirty and not labelled: + print ("PR #" + str(pull.number) + " is dirty and not labelled") + else: + # give some feedback so the user can see we didn't crash + print ("PR #" + str(pull.number) + " OK") |