From e73645505b369fde794fdd8a20bf58096de85f48 Mon Sep 17 00:00:00 2001
From: larsk21 <57503246+larsk21@users.noreply.github.com>
Date: Mon, 31 Jan 2022 19:46:13 +0100
Subject: [PATCH] fix: remove duplicate from interactive highlight test

---
 tests/lean/interactive/highlight.lean.expected.out | 4 ----
 1 file changed, 4 deletions(-)

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}},