Skip to content

Commit cc13c0b

Browse files
author
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for leanprover/lean4#13229
2 parents 7c36ea4 + a1b4b26 commit cc13c0b

2 files changed

Lines changed: 3 additions & 1 deletion

File tree

Batteries/Data/String/Lemmas.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,8 @@ import all Init.Data.String.Legacy -- for unfolding `String.splitOnAux`
2222

2323
@[expose] public section
2424

25+
set_option linter.deprecated false
26+
2527
namespace String
2628

2729
-- TODO(kmill): add `@[ext]` attribute to `String.ext` in core.

lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4-pr-releases:pr-release-13229-aa77588
1+
leanprover/lean4-pr-releases:pr-release-13229-04386e5

0 commit comments

Comments
 (0)