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

chore: style

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-23 14:06:02 -07:00
parent e5601554f9
commit b2bddb5606
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/runtime/io.cpp
View file

@ -342,7 +342,7 @@ extern "C" obj_res lean_io_prim_handle_get_line(b_obj_arg h, obj_arg /* w */) {
return set_io_error(g_io_error_eof);
}
const int buf_sz = 64;
char buf_str[buf_sz];
char buf_str[buf_sz]; // NOLINT
std::string result;
bool first = true;
while (true) {