diff options
| author | Oliver Scherer <github35764891676564198441@oli-obk.de> | 2018-12-23 13:27:37 +0100 |
|---|---|---|
| committer | Oliver Scherer <github35764891676564198441@oli-obk.de> | 2018-12-23 13:27:37 +0100 |
| commit | 488f16a85041e57ce5934df44ed64ffe5303be03 (patch) | |
| tree | 3fb5ff5832a3d104ab4f48c6683bc2963d784339 | |
| parent | b454474c84ed96a8af55ed76e68e428cc11e69c6 (diff) | |
| download | rust-488f16a85041e57ce5934df44ed64ffe5303be03.tar.gz rust-488f16a85041e57ce5934df44ed64ffe5303be03.zip | |
Dedent mergebot message
| -rwxr-xr-x | src/tools/publish_toolstate.py | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/tools/publish_toolstate.py b/src/tools/publish_toolstate.py index 3bf40e336d3..18d447bcdb6 100755 --- a/src/tools/publish_toolstate.py +++ b/src/tools/publish_toolstate.py @@ -70,7 +70,7 @@ def issue( response = urllib2.urlopen(urllib2.Request( gh_url, json.dumps({ - 'body': '''\ + 'body': textwrap.dedent('''\ Hello, this is your friendly neighborhood mergebot. After merging PR {}, I observed that the tool {} no longer builds. A follow-up PR to the repository {} is needed to fix the fallout. @@ -80,7 +80,7 @@ def issue( cc @{}, the PR reviewer, and @rust-lang/compiler -- nominating for prioritization. - '''.format(relevant_pr_number, tool, REPOS[tool], relevant_pr_user, pr_reviewer), + ''').format(relevant_pr_number, tool, REPOS[tool], relevant_pr_user, pr_reviewer), 'title': '`{}` no longer builds after {}'.format(tool, relevant_pr_number), 'assignees': assignees, 'labels': ['T-compiler', 'I-nominated'], |