From 58830be91f37ff611128e7cbf07b156e1fbab854 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 4 Feb 2019 11:11:18 +0100 Subject: [PATCH] chore(library/compiler/emit_cpp): ignore warnings under GCC --- src/library/compiler/emit_cpp.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp index d31896ecf7..61fcbe05a0 100644 --- a/src/library/compiler/emit_cpp.cpp +++ b/src/library/compiler/emit_cpp.cpp @@ -246,6 +246,10 @@ static void emit_file_header(std::ostream & out, module_name const & m, list