From 07ec94b7c2569722093cd118afc0d84c626c938f Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 15 Mar 2023 12:31:56 +0100
Subject: [PATCH] fix strinterpolation again

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

diff --git a/server/leanserver/GameServer/StrInterpolation.lean b/server/leanserver/GameServer/StrInterpolation.lean
index 935e941..db08b36 100644
--- a/server/leanserver/GameServer/StrInterpolation.lean
+++ b/server/leanserver/GameServer/StrInterpolation.lean
@@ -118,7 +118,7 @@ private partial def decodeInterpStrLit (s : String) : Option String :=
     else
       loop i (acc.push c)
   let c := s.get 0
-  if c == '\"' || c == '{' then
+  if c == '\"' || c == '}' then
     loop ⟨1⟩ ""
   else
     loop ⟨0⟩ ""