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

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-06 14:55:27 -07:00
parent 0bfcf434ac
commit 36e032cf94
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/interactive/hover.lean.expected.out
View file

@ -138,7 +138,7 @@ null
{"range":
{"start": {"line": 127, "character": 10},
"end": {"line": 127, "character": 13}},
"contents": {"value": "```lean\nBar.Bar : Type\n```", "kind": "markdown"}}
"contents": {"value": "```lean\nBar : Type\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 129, "character": 4}}
{"range":