diff options
| author | Wladimir J. van der Laan <laanwj@gmail.com> | 2019-01-14 16:32:05 +0100 |
|---|---|---|
| committer | Wladimir J. van der Laan <laanwj@gmail.com> | 2019-01-14 16:32:05 +0100 |
| commit | 059a3cffdfa596aa3adaace3f57fa86fdd3f80fc (patch) | |
| tree | 915e8a2708870eec177c4d5892639031b7f9b15a /contrib/devtools | |
| parent | 035f349371a5b67922ce92c11ad9aa7178fa04f7 (diff) | |
contrib: Detailed reporting for http errors in github-merge
Print detailed error, this makes it easier to diagnose github API issues.
Diffstat (limited to 'contrib/devtools')
| -rwxr-xr-x | contrib/devtools/github-merge.py | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/contrib/devtools/github-merge.py b/contrib/devtools/github-merge.py index 4f827401fb..6712d4f3b6 100755 --- a/contrib/devtools/github-merge.py +++ b/contrib/devtools/github-merge.py @@ -23,6 +23,7 @@ import sys import json import codecs from urllib.request import Request, urlopen +from urllib.error import HTTPError # External tools (can be overridden using environment) GIT = os.getenv('GIT','git') @@ -57,6 +58,11 @@ def retrieve_pr_info(repo,pull): reader = codecs.getreader('utf-8') obj = json.load(reader(result)) return obj + except HTTPError as e: + error_message = e.read() + print('Warning: unable to retrieve pull information from github: %s' % e) + print('Detailed error: %s' % error_message) + return None except Exception as e: print('Warning: unable to retrieve pull information from github: %s' % e) return None |