max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(msvc): remove another \uXX char that was causing an infinite loop

Browse source
This commit is contained in:
Nuno Lopes 2018-02-08 17:42:26 +00:00 • committed by Leonardo de Moura
parent 977e11f9be
commit c43ebd8bf7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/pp.cpp
View file

@ -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