From 42ee42b7324c9051b6a1f736c3357363682cf34d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Feb 2019 14:15:38 -0800 Subject: [PATCH] fix(library/compiler/emit_cpp): bug at quote_string --- src/library/compiler/emit_cpp.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp index 40c99ef0d5..337c4abbfa 100644 --- a/src/library/compiler/emit_cpp.cpp +++ b/src/library/compiler/emit_cpp.cpp @@ -255,6 +255,8 @@ static void emit_quoted_string(std::ostream & out, std::string const & s) { out << "\\t"; else if (c == '\\') out << "\\\\"; + else if (c == '\"') + out << "\\\""; else if (c <= 31 || c >= 0x7f) { out << "\\x"; emit_hexdigit(out, c / 16); emit_hexdigit(out, c % 16); } else {