From 018020d36fb16b01045cefb2e0a960f6e8e759f9 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Mon, 18 Sep 2023 05:39:04 -0400
Subject: [PATCH] fix: uninterpolated error message in `registerRpcProcedure`
 (#2547)

---
 src/Lean/Server/Rpc/RequestHandling.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean
index 2c7293329f..44d67cba55 100644
--- a/src/Lean/Server/Rpc/RequestHandling.lean
+++ b/src/Lean/Server/Rpc/RequestHandling.lean
@@ -104,11 +104,11 @@ def registerBuiltinRpcProcedure (method : Name) paramType respType
 open Lean Elab Command Term Meta in
 def registerRpcProcedure (method : Name) : CoreM Unit := do
   let env ← getEnv
-  let errMsg := "Failed to register RPC call handler for '{method}'"
+  let errMsg := m!"Failed to register RPC call handler for '{method}'"
   if (←builtinRpcProcedures.get).contains method then
-    throwError s!"{errMsg}: already registered (builtin)"
+    throwError m!"{errMsg}: already registered (builtin)"
   if userRpcProcedures.contains env method then
-    throwError s!"{errMsg}: already registered"
+    throwError m!"{errMsg}: already registered"
   let wrappedName := method ++ `_rpc_wrapped
   let procT := mkConst ``RpcProcedure
   let proc ← MetaM.run' <| TermElabM.run' <| withoutErrToSorry do