Skip to content

Commit dbe837b

Browse files
committed
fix(TextBased): use endPos instead of rawEndPos
String.rawEndPos now returns String.Pos.Raw instead of s.Pos. String.find returns s.Pos, so we need to compare with endPos.
1 parent a1e8445 commit dbe837b

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Mathlib/Tactic/Linter/TextBased.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -262,7 +262,7 @@ def nonbreakingSpaceLinter : TextbasedLinter := fun opts lines ↦ Id.run do
262262
for h : idx in [:lines.size] do
263263
let line := lines[idx]
264264
let pos := line.find (· == ' ')
265-
if pos != line.rawEndPos then
265+
if pos != line.endPos then
266266
errors := errors.push (StyleError.nonbreakingSpace, idx + 1)
267267
return (errors, none)
268268

0 commit comments

Comments
 (0)