From 2edde7b3765a74efc9124981a44ba154339f41e0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 25 Feb 2024 09:38:43 -0800
Subject: [PATCH] chore: `initialize` => `builtin_initialize`

---
 src/Lean/Server/CodeActions/Attr.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Server/CodeActions/Attr.lean b/src/Lean/Server/CodeActions/Attr.lean
index a49e69d2a4..2c63f2a95a 100644
--- a/src/Lean/Server/CodeActions/Attr.lean
+++ b/src/Lean/Server/CodeActions/Attr.lean
@@ -32,7 +32,7 @@ def mkHoleCodeAction (n : Name) : ImportM HoleCodeAction := do
   IO.ofExcept <| unsafe env.evalConstCheck HoleCodeAction opts ``HoleCodeAction n
 
 /-- An extension which collects all the hole code actions. -/
-initialize holeCodeActionExt :
+builtin_initialize holeCodeActionExt :
     PersistentEnvExtension Name (Name × HoleCodeAction) (Array Name × Array HoleCodeAction) ←
   registerPersistentEnvExtension {
     mkInitial := pure (#[], #[])
@@ -42,7 +42,7 @@ initialize holeCodeActionExt :
     exportEntriesFn := (·.1)
   }
 
-initialize
+builtin_initialize
   registerBuiltinAttribute {
     name := `hole_code_action
     descr := "Declare a new hole code action, to appear in the code actions on ?_ and _"
@@ -92,7 +92,7 @@ def CommandCodeActions.insert (self : CommandCodeActions)
         m.insert a ((m.findD a #[]).push action) }
 
 /-- An extension which collects all the command code actions. -/
-initialize cmdCodeActionExt :
+builtin_initialize cmdCodeActionExt :
     PersistentEnvExtension CommandCodeActionEntry (CommandCodeActionEntry × CommandCodeAction)
       (Array CommandCodeActionEntry × CommandCodeActions) ←
   registerPersistentEnvExtension {
@@ -118,7 +118,7 @@ This attribute marks a code action, which is used to suggest new tactics or repl
 -/
 syntax (name := command_code_action) "command_code_action" (ppSpace ident)* : attr
 
-initialize
+builtin_initialize
   registerBuiltinAttribute {
     name := `command_code_action
     descr := "Declare a new command code action, to appear in the code actions on commands"