From c43ebd8bf7c41878e09c2f501833ebe8107c0160 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 8 Feb 2018 17:42:26 +0000 Subject: [PATCH] fix(msvc): remove another \uXX char that was causing an infinite loop --- src/frontends/lean/pp.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 13701ec51b..9217f70c11 100755 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -124,7 +124,7 @@ bool pp_using_anonymous_constructor(environment const & env, name const & n) { } void initialize_pp() { - g_ellipsis_n_fmt = new format(highlight(format("\u2026"))); + g_ellipsis_n_fmt = new format(highlight(format("\xE2\x80\xA6"))); //\u2026 g_ellipsis_fmt = new format(highlight(format("..."))); g_placeholder_fmt = new format(highlight(format("_"))); g_lambda_n_fmt = new format(highlight_keyword(format("\xCE\xBB"))); //\u03BB