rename maybe_delink to maybe_remove_mention

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