use translation of level title

2024-04-06 14:56:19 +02:00
parent 3124d90cd6
commit 9b05a27888
2 changed files with 2 additions and 2 deletions
@@ -42,7 +42,7 @@ elab "Title" t:str : command => do
  | .Level => modifyCurLevel fun level => pure {level with title := title}
  | .World => modifyCurWorld  fun world => pure {world with title := title}
  | .Game => modifyCurGame  fun game => pure {game with
-      title := t.getString
+      title := title
      tile := {game.tile with title := title}}

 /-- Define the introduction of the current game/world/level. -/