From 003835111dde6f01c5432a419eda249ba3d45e15 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Feb 2024 18:04:27 -0800 Subject: [PATCH] chore: fix tests --- tests/lean/1021.lean.expected.out | 8 ++++---- tests/lean/run/sharecommon.lean | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out index f3853cafdc..1eaf8c6869 100644 --- a/tests/lean/1021.lean.expected.out +++ b/tests/lean/1021.lean.expected.out @@ -1,8 +1,8 @@ -some { range := { pos := { line := 189, column := 42 }, +some { range := { pos := { line := 177, column := 42 }, charUtf16 := 42, - endPos := { line := 195, column := 31 }, + endPos := { line := 183, column := 31 }, endCharUtf16 := 31 }, - selectionRange := { pos := { line := 189, column := 46 }, + selectionRange := { pos := { line := 177, column := 46 }, charUtf16 := 46, - endPos := { line := 189, column := 58 }, + endPos := { line := 177, column := 58 }, endCharUtf16 := 58 } } diff --git a/tests/lean/run/sharecommon.lean b/tests/lean/run/sharecommon.lean index c4db313573..1348e4c752 100644 --- a/tests/lean/run/sharecommon.lean +++ b/tests/lean/run/sharecommon.lean @@ -2,7 +2,7 @@ import Lean.Util.ShareCommon open Lean.ShareCommon def check (b : Bool) : ShareCommonT IO Unit := do -unless b do throw $ IO.userError "check failed" + unless b do throw $ IO.userError "check failed" unsafe def tst1 : ShareCommonT IO Unit := do let x := [1]