From bc8511ccbf9ff786c5abc3f788e8c7b6188071fe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 25 Feb 2024 10:42:21 -0800
Subject: [PATCH] chore: `builtin_command_code_action` for `#guard_msgs`

---
 src/Lean/Elab/GuardMsgs.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean
index ea4d3aa17d..a9f8bce381 100644
--- a/src/Lean/Elab/GuardMsgs.lean
+++ b/src/Lean/Elab/GuardMsgs.lean
@@ -100,7 +100,7 @@ deriving TypeName
 
 open CodeAction Server RequestM in
 /-- A code action which will update the doc comment on a `#guard_msgs` invocation. -/
-@[command_code_action guardMsgsCmd]
+@[builtin_command_code_action guardMsgsCmd]
 def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
   let .node _ ts := node | return #[]
   let res := ts.findSome? fun