max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update line numbers in test after rebase

Browse source
This commit is contained in:
Scott Morrison 2024-02-09 18:22:39 +11:00 • committed by Sebastian Ullrich
parent 003835111d
commit a7364499d2
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
tests/lean/1021.lean.expected.out
View file

@ -1,8 +1,8 @@
some { range := { pos := { line := 177, column := 42 },
some { range := { pos := { line := 191, column := 42 },
charUtf16 := 42,
endPos := { line := 183, column := 31 },
endPos := { line := 197, column := 31 },
endCharUtf16 := 31 },
selectionRange := { pos := { line := 177, column := 46 },
selectionRange := { pos := { line := 191, column := 46 },
charUtf16 := 46,
endPos := { line := 177, column := 58 },
endPos := { line := 191, column := 58 },
endCharUtf16 := 58 } }