From 1b78cb4836cf626007bd38872956a6fab8910993 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 9 Jul 2024 22:35:22 +0200
Subject: [PATCH] chore: fix test output

---
 .../lean/interactive/incrementalTactic.lean.expected.out  | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/tests/lean/interactive/incrementalTactic.lean.expected.out b/tests/lean/interactive/incrementalTactic.lean.expected.out
index 706ae32c688f..044df6c6ebf0 100644
--- a/tests/lean/interactive/incrementalTactic.lean.expected.out
+++ b/tests/lean/interactive/incrementalTactic.lean.expected.out
@@ -98,17 +98,17 @@ s
   {"source": "Lean 4",
    "severity": 1,
    "range":
-   {"start": {"line": 3, "character": 4}, "end": {"line": 3, "character": 10}},
+   {"start": {"line": 3, "character": 4}, "end": {"line": 3, "character": 5}},
    "message": "no goals to be solved",
    "fullRange":
-   {"start": {"line": 3, "character": 4}, "end": {"line": 3, "character": 10}}},
+   {"start": {"line": 3, "character": 4}, "end": {"line": 3, "character": 5}}},
   {"source": "Lean 4",
    "severity": 1,
    "range":
-   {"start": {"line": 4, "character": 2}, "end": {"line": 4, "character": 8}},
+   {"start": {"line": 4, "character": 2}, "end": {"line": 4, "character": 3}},
    "message": "no goals to be solved",
    "fullRange":
-   {"start": {"line": 4, "character": 2}, "end": {"line": 4, "character": 8}}}]}
+   {"start": {"line": 4, "character": 2}, "end": {"line": 4, "character": 3}}}]}
 {"version": 2,
  "uri": "file:///incrementalTactic.lean",
  "diagnostics":