From b3c89070e38423d69ab901db584ffaa1c3bd67f9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Oct 2015 09:57:58 -0700 Subject: [PATCH] fix(tests/lean): test output --- tests/lean/bad_quoted_symbol.lean.expected.out | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/lean/bad_quoted_symbol.lean.expected.out b/tests/lean/bad_quoted_symbol.lean.expected.out index 720e88dfe..6f183e561 100644 --- a/tests/lean/bad_quoted_symbol.lean.expected.out +++ b/tests/lean/bad_quoted_symbol.lean.expected.out @@ -1,5 +1,5 @@ -tests/lean/bad_quoted_symbol.lean:2:12: error: first character of a quoted symbols cannot be a digit -tests/lean/bad_quoted_symbol.lean:3:16: error: unexpected space inside of quoted symbol -tests/lean/bad_quoted_symbol.lean:4:14: error: unexpected end of quoted symbol -tests/lean/bad_quoted_symbol.lean:5:10: error: invalid quoted symbol, invalid character -tests/lean/bad_quoted_symbol.lean:5:10: error: invalid notation declaration, symbol expected +bad_quoted_symbol.lean:2:12: error: first character of a quoted symbols cannot be a digit +bad_quoted_symbol.lean:3:16: error: unexpected space inside of quoted symbol +bad_quoted_symbol.lean:4:14: error: unexpected end of quoted symbol +bad_quoted_symbol.lean:5:10: error: invalid quoted symbol, invalid character +bad_quoted_symbol.lean:5:10: error: invalid notation declaration, symbol expected