Skip to content

Commit fbe98d7

Browse files
authored
fix: turn meta import into import in Init.Data.ToString (#10754)
This PR makes sure that we always properly import `Init.Data.ToString.Name` when importing `Init`.
1 parent 9a5e425 commit fbe98d7

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/Data/ToString.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,4 +8,4 @@ module
88
prelude
99
public import Init.Data.ToString.Basic
1010
public import Init.Data.ToString.Macro
11-
public meta import Init.Data.ToString.Name
11+
public import Init.Data.ToString.Name

0 commit comments

Comments
 (0)