mirror of
https://github.com/rust-lang/rust.git
synced 2025-06-06 12:18:33 +00:00
rename maybe_delink to maybe_remove_mention
This commit is contained in:
parent
f470c29936
commit
c37e72897c
@ -86,7 +86,7 @@ def gh_url():
|
|||||||
return os.environ['TOOLSTATE_ISSUES_API_URL']
|
return os.environ['TOOLSTATE_ISSUES_API_URL']
|
||||||
|
|
||||||
|
|
||||||
def maybe_unlink(message):
|
def maybe_remove_mention(message):
|
||||||
# type: (str) -> str
|
# type: (str) -> str
|
||||||
if os.environ.get('TOOLSTATE_SKIP_MENTIONS') is not None:
|
if os.environ.get('TOOLSTATE_SKIP_MENTIONS') is not None:
|
||||||
return message.replace("@", "")
|
return message.replace("@", "")
|
||||||
@ -109,7 +109,7 @@ def issue(
|
|||||||
else:
|
else:
|
||||||
status_description = 'no longer builds'
|
status_description = 'no longer builds'
|
||||||
request = json.dumps({
|
request = json.dumps({
|
||||||
'body': maybe_unlink(textwrap.dedent('''\
|
'body': maybe_remove_mention(textwrap.dedent('''\
|
||||||
Hello, this is your friendly neighborhood mergebot.
|
Hello, this is your friendly neighborhood mergebot.
|
||||||
After merging PR {}, I observed that the tool {} {}.
|
After merging PR {}, I observed that the tool {} {}.
|
||||||
A follow-up PR to the repository {} is needed to fix the fallout.
|
A follow-up PR to the repository {} is needed to fix the fallout.
|
||||||
@ -285,7 +285,7 @@ try:
|
|||||||
issue_url = gh_url() + '/{}/comments'.format(number)
|
issue_url = gh_url() + '/{}/comments'.format(number)
|
||||||
response = urllib2.urlopen(urllib2.Request(
|
response = urllib2.urlopen(urllib2.Request(
|
||||||
issue_url,
|
issue_url,
|
||||||
json.dumps({'body': maybe_unlink(message)}).encode(),
|
json.dumps({'body': maybe_remove_mention(message)}).encode(),
|
||||||
{
|
{
|
||||||
'Authorization': 'token ' + github_token,
|
'Authorization': 'token ' + github_token,
|
||||||
'Content-Type': 'application/json',
|
'Content-Type': 'application/json',
|
||||||
|
Loading…
Reference in New Issue
Block a user