remove deprecated comment

2023-07-29 12:28:54 +02:00
parent ee7915a98f
commit 34009bcc17
1 changed files with 1 additions and 1 deletions
@@ -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.