michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update format.cpp, flatten(LINE) = "" instead of " "

Browse source
This commit is contained in:
Soonho Kong 2013-08-01 18:53:41 -07:00
parent e898bb996c
commit 229b4f8759
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/util/format.cpp
View file

@ -91,7 +91,7 @@ sexpr format::flatten(sexpr const & s) {
/* flatten (x <|> y) = flatten x */
return flatten(sexpr_choice_1(s));
case format_kind::LINE:
return sexpr_text(sexpr(" "));
return sexpr_text(sexpr(""));
case format_kind::TEXT:
case format_kind::COLOR_BEGIN:
case format_kind::COLOR_END: