aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-12-30 20:06:26 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-01-08 11:52:38 +0100
commit17067aac03eabb8369d587dc91b622642b2673f8 (patch)
treec6e3ab448914d44221fe4fdf64dc0ab33773341c /dev
parent2b28380d1d04c0dc2d0899ba3f3489e29015a6fa (diff)
github-check-prs.py: command line option to get token from a file
Diffstat (limited to 'dev')
-rwxr-xr-xdev/tools/github-check-prs.py18
1 files changed, 16 insertions, 2 deletions
diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py
index 9688308d9..74325d3ee 100755
--- a/dev/tools/github-check-prs.py
+++ b/dev/tools/github-check-prs.py
@@ -4,13 +4,27 @@
# 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"
-token = input("Github access token: ")
+parser = argparse.ArgumentParser()
+parser.add_argument("--token-file", type=argparse.FileType('r'))
+args = parser.parse_args()
-g = Github(token)
+if args.token_file is None:
+ token = input("Github access token: ")
+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)