From 9a69c48cb23f313e5986e87a8867eaf3d9b6528e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 20:42:05 -0800 Subject: [PATCH] fix: Integration test failure --- Test/Integration.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Test/Integration.lean b/Test/Integration.lean index 9fb86b7..171bc91 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -222,6 +222,7 @@ def test_frontend_process_sorry : Test := boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize), goalStateId? := .some 0, goals := #[goal1], + goalSrcBoundaries := #[(57, 62)], messages := #[":2:0: warning: declaration uses 'sorry'\n"], }], }: Protocol.FrontendProcessResult),