diff options
| author | Oliver Scherer <github35764891676564198441@oli-obk.de> | 2018-12-20 14:29:42 +0100 |
|---|---|---|
| committer | Oliver Scherer <github35764891676564198441@oli-obk.de> | 2018-12-20 14:29:42 +0100 |
| commit | b454474c84ed96a8af55ed76e68e428cc11e69c6 (patch) | |
| tree | 709db066663a699afc4a72cfd75dfc1244e5979a | |
| parent | a4c317ef980a8c0ef443937c78143535781e791c (diff) | |
| download | rust-b454474c84ed96a8af55ed76e68e428cc11e69c6.tar.gz rust-b454474c84ed96a8af55ed76e68e428cc11e69c6.zip | |
Tidy
| -rwxr-xr-x | src/tools/publish_toolstate.py | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/tools/publish_toolstate.py b/src/tools/publish_toolstate.py index fbb3bc9a751..3bf40e336d3 100755 --- a/src/tools/publish_toolstate.py +++ b/src/tools/publish_toolstate.py @@ -75,7 +75,8 @@ def issue( After merging PR {}, I observed that the tool {} no longer builds. A follow-up PR to the repository {} is needed to fix the fallout. - cc @{}, do you think you would have time to do the follow-up work? If so, that would be great! + cc @{}, do you think you would have time to do the follow-up work? + If so, that would be great! cc @{}, the PR reviewer, and @rust-lang/compiler -- nominating for prioritization. @@ -144,7 +145,10 @@ def update_latest( build_failed = True if build_failed: - issue(tool, MAINTAINERS.get(tool), relevant_pr_number, relevant_pr_user, pr_reviewer) + issue( + tool, MAINTAINERS.get(tool), + relevant_pr_number, relevant_pr_user, pr_reviewer, + ) if changed: status['commit'] = current_commit @@ -168,7 +172,10 @@ if __name__ == '__main__': github_token = sys.argv[4] # assume that PR authors are also owners of the repo where the branch lives - relevant_pr_match = re.search('Auto merge of #([0-9]+) - ([^:]+):[^,]+ r=([^\s]+)', cur_commit_msg) + relevant_pr_match = re.search( + 'Auto merge of #([0-9]+) - ([^:]+):[^,]+ r=([^\s]+)', + cur_commit_msg, + ) if relevant_pr_match: number = relevant_pr_match.group(1) relevant_pr_user = relevant_pr_match.group(2) |
