Skip to content

Commit e97c150

Browse files
authored
fix: shake: register attribute rev use independent of initialize kind (#11293)
1 parent b6399e1 commit e97c150

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Lean/Elab/Attributes.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
5858
let .ok _impl := getAttributeImpl (← getEnv) attrName
5959
| throwError "Unknown attribute `[{attrName}]`"
6060
if let .ok impl := getAttributeImpl (← getEnv) attrName then
61-
if isIOUnitRegularInitFn (← getEnv) impl.ref then -- skip `builtin_initialize` attributes
61+
if regularInitAttr.getParam? (← getEnv) impl.ref |>.isSome then -- skip `builtin_initialize` attributes
6262
recordExtraModUseFromDecl (isMeta := true) impl.ref
6363
/- The `AttrM` does not have sufficient information for expanding macros in `args`.
6464
So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/

0 commit comments

Comments
 (0)