From 34009bcc172eac808ddbdb98f06411ad010ec9e4 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Sat, 29 Jul 2023 12:28:54 +0200
Subject: [PATCH] remove deprecated comment

---
 server/GameServer/Commands.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index cb3db37..f1b9b42 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -741,7 +741,7 @@ elab "MakeGame" : command => do
     | "" =>
       -- If documentation is missing, try using the docstring instead.
       match docstring with
-      | some ds => s!"*(lean docstring)*\\\n{ds}" -- TODO `\n` does not work in markdown
+      | some ds => s!"*(lean docstring)*\\\n{ds}"
       | none => "(missing)"
     | template =>
       -- TODO: Process content template.