From d420f4643289e799bc3e4c3ff08db2345955f796 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 20 May 2020 15:13:24 +0200 Subject: [PATCH] fix: '\r' escape --- src/Init/Lean/Parser/Parser.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index 9ea5742b2b..78723126fa 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -619,7 +619,7 @@ def quotedCharFn : ParserFn if input.atEnd i then s.mkEOIError else let curr := input.get i; - if curr == '\\' || curr == '\"' || curr == '\'' || curr == 'n' || curr == 't' then + if curr == '\\' || curr == '\"' || curr == '\'' || curr == 'r' || curr == 'n' || curr == 't' then s.next input i else if curr == 'x' then andthenFn hexDigitFn hexDigitFn c (s.next input i)