From 36e032cf9489f34fa9dd002b28a8b9da29960000 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Apr 2022 14:55:27 -0700
Subject: [PATCH] chore: fix test

---
 tests/lean/interactive/hover.lean.expected.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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":