diff --git a/tools/ci_tools.py b/tools/ci_tools.py index e5ca0c2c28..aeb367af38 100644 --- a/tools/ci_tools.py +++ b/tools/ci_tools.py @@ -19,7 +19,10 @@ def get_release_type_github(Log, github_token): match = re.search("pull request #(\d+)", line) if match: pr_number = match.group(1) - pr = repo.get_pull(int(pr_number)) + try: + pr = repo.get_pull(int(pr_number)) + except: + continue for label in pr.labels: labels.add(label.name)