diff --git a/tests/lean/interactive/highlight.lean.expected.out b/tests/lean/interactive/highlight.lean.expected.out index d24c11d7aa..859c77de75 100644 --- a/tests/lean/interactive/highlight.lean.expected.out +++ b/tests/lean/interactive/highlight.lean.expected.out @@ -19,10 +19,6 @@ {"start": {"line": 18, "character": 23}, "end": {"line": 18, "character": 26}}, "kind": 1}, - {"range": - {"start": {"line": 22, "character": 16}, - "end": {"line": 22, "character": 19}}, - "kind": 1}, {"range": {"start": {"line": 22, "character": 16}, "end": {"line": 22, "character": 19}},