fix

datokrat · datokrat · commit 15482bcc28f2 · 2025-06-23T23:19:20.000+02:00
diff --git a/tests/lean/ellipsisProjIssue.lean.expected.out b/tests/lean/ellipsisProjIssue.lean.expected.out
@@ -3,4 +3,3 @@ ellipsisProjIssue.lean:1:18-1:22: error: unknown identifier 'succ'
   upper :=
     sorry } : Std.PRange { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.open }
   (Nat → Nat → Nat)
-ellipsisProjIssue.lean:1:18-1:22: error: unexpected identifier; expected command
