diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index 796c29e61f..8d8f445256 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -475,7 +475,8 @@ def quoteString (s : String) : String := let q := s.foldl (fun q c => q ++ if c == '\n' then "\\n" - else if c == '\n' then "\\t" + else if c == '\r' then "\\r" + else if c == '\t' then "\\t" else if c == '\\' then "\\\\" else if c == '\"' then "\\\"" else if c.toNat <= 31 then diff --git a/tests/compiler/escape.lean b/tests/compiler/escape.lean new file mode 100644 index 0000000000..e6d71faa33 --- /dev/null +++ b/tests/compiler/escape.lean @@ -0,0 +1,3 @@ +def main : IO Unit := do + IO.eprintln $ "\rfailed at counter-example" + IO.eprintln $ "\tfailed at counter-example" diff --git a/tests/compiler/escape.lean.expected.out b/tests/compiler/escape.lean.expected.out new file mode 100644 index 0000000000..9c31d16cee --- /dev/null +++ b/tests/compiler/escape.lean.expected.out @@ -0,0 +1,2 @@ + failed at counter-example + failed at counter-example