From 1dd93b34ad94b925f44cb448f77db902aaa0b56c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Aug 2016 17:22:16 -0700 Subject: [PATCH] chore(frontends/lean/print_cmd): compilation error on g++ 8.2 --- src/frontends/lean/print_cmd.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index abb29e5189..815e842d04 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -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();