From c059992ec852e3c23f02dd17c9d3ef32dec87012 Mon Sep 17 00:00:00 2001
From: Danny Ben-David <dannybd@users.noreply.github.com>
Date: Mon, 28 Dec 2020 18:06:50 -0500
Subject: [PATCH] [tweak] "Game for {user.mention}:"

`user.display_name` doesn't tag the user who requested the game. Using `user.mention` makes at tags, which also means users can search for games using Discord search (`Game for mentions:@foobar`)
---
 the_prestige.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/the_prestige.py b/the_prestige.py
index 0596ab0..a1703ae 100644
--- a/the_prestige.py
+++ b/the_prestige.py
@@ -553,7 +553,7 @@ async def watch_game(channel, newgame, user = None):
     in_emoji = discord.utils.get(client.emojis, id = 791578957244792832)
 
     if user is not None:
-        await channel.send(f"Game for {user.display_name}:")
+        await channel.send(f"Game for {user.mention}:")
     embed = await channel.send("Starting...")
     await asyncio.sleep(1)
     await embed.pin()