From f37fd97d9f296417639dd4b39ddf690dc8a5b262 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 Nov 2020 18:34:38 -0800 Subject: [PATCH] chore: fix test --- tests/lean/exitAfterParseError.lean.expected.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/exitAfterParseError.lean.expected.out b/tests/lean/exitAfterParseError.lean.expected.out index 8e6c29a13b..87d0dd244a 100644 --- a/tests/lean/exitAfterParseError.lean.expected.out +++ b/tests/lean/exitAfterParseError.lean.expected.out @@ -1 +1 @@ -exitAfterParseError.lean:5:0: error: expected ':=' or '|' +exitAfterParseError.lean:5:0: error: expected ':=', 'where' or '|'