From 2c1e69611bf19dc58aab67761ba5b755c8c93067 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 24 Jul 2024 11:06:21 +0200 Subject: [PATCH] Update Commands.lean --- server/GameServer/Commands.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 76544f9..e30c426 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -119,7 +119,7 @@ elab "Languages" t:str* : command => do modifyCurGame fun game => pure {game with tile := {game.tile with languages := t.map (·.getString) |>.toList}} -/-- The Image of the game (optional). TODO: Not impementeds -/ +/-- The Image of the game (optional). TODO: Not implemented -/ elab "CoverImage" t:str : command => do let file := t.getString if not <| ← System.FilePath.pathExists file then @@ -610,7 +610,7 @@ where filterArgs (args : List Syntax) : List Syntax := | Syntax.node _ `GameServer.Tactic.Hint _ :: _ :: r | Syntax.node _ `GameServer.Tactic.Branch _ :: _ :: r => filterArgs r - -- delete `Hint` and `Branch` occurence at the end of the tactic sequence. + -- delete `Hint` and `Branch` occurrence at the end of the tactic sequence. | Syntax.node _ `GameServer.Tactic.Hint _ :: [] | Syntax.node _ `GameServer.Tactic.Branch _ :: [] => []