Skip to content

Commit 8754f96

Browse files
committed
fix test
1 parent 4007930 commit 8754f96

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

tests/lean/run/extraModUses.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -173,7 +173,7 @@ References from `@[grind]` are tracked (here `List.append` from Init.Prelude)
173173
attribute [grind =] List.append
174174

175175
/--
176-
info: Entries: [import Init.Grind.Attr, public import Init.Prelude]
176+
info: Entries: [import Init.Grind.Attr, public import Init.Prelude, import Init.Prelude]
177177
Is rev mod use: false
178178
-/
179179
#guard_msgs in #eval showExtraModUses

0 commit comments

Comments
 (0)