diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index dce7d878b3..68d6fd0db1 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -192,7 +192,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
   if let Info.ofFieldInfo fi := i then
     return ← findDocString? env fi.projName
   if let some ei := i.toElabInfo? then
-    return ← findDocString? env ei.elaborator <||> findDocString? env ei.stx.getKind
+    return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator
   return none
 
 /-- Construct a hover popup, if any, from an info node in a context.-/
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index 6d33c26f9a..1f18a01d81 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -76,12 +76,12 @@
  "position": {"line": 36, "character": 2}}
 {"range":
  {"start": {"line": 36, "character": 2}, "end": {"line": 36, "character": 23}},
- "contents": {"value": "My way better tactic ", "kind": "markdown"}}
+ "contents": {"value": "My tactic ", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 44, "character": 2}}
 {"range":
  {"start": {"line": 44, "character": 2}, "end": {"line": 44, "character": 23}},
- "contents": {"value": "My way better tactic ", "kind": "markdown"}}
+ "contents": {"value": "My tactic ", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 51, "character": 7}}
 {"range":
@@ -93,8 +93,7 @@
 {"range":
  {"start": {"line": 58, "character": 7}, "end": {"line": 58, "character": 15}},
  "contents":
- {"value": "```lean\nNat\n```\n***\nMy way better notation ",
-  "kind": "markdown"}}
+ {"value": "```lean\nNat\n```\n***\nMy notation ", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 68, "character": 7}}
 {"range":
@@ -124,7 +123,7 @@
  "position": {"line": 86, "character": 2}}
 {"range":
  {"start": {"line": 86, "character": 0}, "end": {"line": 86, "character": 7}},
- "contents": {"value": "My way better command ", "kind": "markdown"}}
+ "contents": {"value": "My command ", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 89, "character": 16}}
 {"range":