chore: fix test output

leanprover · Jul 9, 2024 · 1b78cb4 · 1b78cb4
1 parent f2e4dbd
commit 1b78cb4
Showing 1 changed file with 4 additions and 4 deletions.
diff --git 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":