diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index bffd202095..563e4293c4 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -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":