From 17067aac03eabb8369d587dc91b622642b2673f8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 30 Dec 2017 20:06:26 +0100
Subject: github-check-prs.py: command line option to get token from a file

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

(limited to 'dev/tools/github-check-prs.py')

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)
 
-- 
cgit v1.2.3