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

chore(frontends/lean/print_cmd): compilation error on g++ 8.2

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-05 17:22:16 -07:00
parent 38524475c9
commit 1dd93b34ad
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/print_cmd.cpp
View file

@ -253,7 +253,7 @@ static void print_attributes(parser const & p, name const & n) {
return a1->get_name() < a2->get_name();
});
for (auto attr : attrs) {
if (strcmp(attr->get_name(), "reducibility") == 0)
if (attr->get_name() == "reducibility")
continue;
if (auto data = attr->get(env, n)) {
out << " [" << attr->get_name();