diff options
Diffstat (limited to 'src/tools/publish_toolstate.py')
| -rwxr-xr-x | src/tools/publish_toolstate.py | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/tools/publish_toolstate.py b/src/tools/publish_toolstate.py index bad86701dae..2018c239ba0 100755 --- a/src/tools/publish_toolstate.py +++ b/src/tools/publish_toolstate.py @@ -86,7 +86,7 @@ def gh_url(): return os.environ['TOOLSTATE_ISSUES_API_URL'] -def maybe_unlink(message): +def maybe_remove_mention(message): # type: (str) -> str if os.environ.get('TOOLSTATE_SKIP_MENTIONS') is not None: return message.replace("@", "") @@ -109,7 +109,7 @@ def issue( else: status_description = 'no longer builds' request = json.dumps({ - 'body': maybe_unlink(textwrap.dedent('''\ + 'body': maybe_remove_mention(textwrap.dedent('''\ Hello, this is your friendly neighborhood mergebot. After merging PR {}, I observed that the tool {} {}. 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) response = urllib2.urlopen(urllib2.Request( issue_url, - json.dumps({'body': maybe_unlink(message)}).encode(), + json.dumps({'body': maybe_remove_mention(message)}).encode(), { 'Authorization': 'token ' + github_token, 'Content-Type': 'application/json', |