From 4bf5c45865b86d8f95fb3f435aeecb229b9ef705 Mon Sep 17 00:00:00 2001
From: LeSeulArtichaut <leseulartichaut@gmail.com>
Date: Mon, 28 Sep 2020 22:28:47 +0200
Subject: [PATCH] Remove outdated line from `publish_toolstate` hook

---
 src/tools/publish_toolstate.py | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/tools/publish_toolstate.py b/src/tools/publish_toolstate.py
index 9cfde0c232b..33613e2dc10 100755
--- a/src/tools/publish_toolstate.py
+++ b/src/tools/publish_toolstate.py
@@ -157,9 +157,6 @@ def issue(
 
         cc @{}, do you think you would have time to do the follow-up work?
         If so, that would be great!
-
-        And nominating for compiler team prioritization.
-
         ''').format(
             relevant_pr_number, tool, status_description,
             REPOS.get(tool), relevant_pr_user