bjoernager/rust
bjoernager/rust
1
Fork 0
Code Activity

Dedent mergebot message

Browse source
This commit is contained in:
Oliver Scherer 2018-12-23 13:27:37 +01:00
parent b454474c84
commit 488f16a850
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tools/publish_toolstate.py
View file

@ -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'],