From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- dev/tools/github-check-prs.py | 47 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100755 dev/tools/github-check-prs.py (limited to 'dev/tools/github-check-prs.py') diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py new file mode 100755 index 00000000..beb26d91 --- /dev/null +++ b/dev/tools/github-check-prs.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python3 + +# Requires PyGithub https://pypi.python.org/pypi/PyGithub, for instance +# debian package: python3-github +# nix: nix-shell -p python3 python3Packages.PyGithub --run ./github-check-rebase.py +from github import Github +import argparse + +REPO = "coq/coq" +REBASE_LABEL="needs: rebase" + +parser = argparse.ArgumentParser() +parser.add_argument("--token-file", type=argparse.FileType('r')) +args = parser.parse_args() + +if args.token_file is None: + token = input("Github access token: ").strip() +else: + token = args.token_file.read().rstrip("\n") + args.token_file.close() + +if token == "": + print ("Warning: using the GitHub API without a token") + print ("We may run into rate limit issues") + g = Github() +else: + 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") + 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