chore(library/compiler/csimp): disable bogus warning

2018-09-24 08:41:07 -07:00 · 2018-09-24 08:41:07 -07:00 · ac90dba90f
commit ac90dba90f
parent 7f00149338
1 changed files with 4 additions and 0 deletions
--- a/src/library/compiler/csimp.cpp
+++ b/src/library/compiler/csimp.cpp
@ -94,6 +94,10 @@ class csimp_fn {
            }
        }
        lean_assert(i == minors_begin);
+        /* The following #pragma is to disable a bogus g++ 4.9 warning at `optional<unsigned> r` */
+        #if defined(__GNUC__) && !defined(__CLANG__)
+        #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
+        #endif
        optional<unsigned> r;
        for (; i < minors_end; i++) {
            expr minor = args[i];