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

chore(library/compiler/emit_cpp): ignore warnings under GCC

Browse source
This commit is contained in:
Sebastian Ullrich 2019-02-04 11:11:18 +01:00 • committed by Leonardo de Moura
parent 34110945f2
commit 58830be91f
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/compiler/emit_cpp.cpp
View file

@ -246,6 +246,10 @@ static void emit_file_header(std::ostream & out, module_name const & m, list<mod
out << "#if defined(__clang__)\n";
out << "#pragma clang diagnostic ignored \"-Wunused-parameter\"\n";
out << "#pragma clang diagnostic ignored \"-Wunused-label\"\n";
out << "#elif defined(__GNUC__) && !defined(__CLANG__)\n";
out << "#pragma GCC diagnostic ignored \"-Wunused-parameter\"\n";
out << "#pragma GCC diagnostic ignored \"-Wunused-label\"\n";
out << "#pragma GCC diagnostic ignored \"-Wunused-but-set-variable\"\n";
out << "#endif\n";
}