diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index a620d86672..c9b4eecf98 100644 --- 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 r` */ + #if defined(__GNUC__) && !defined(__CLANG__) + #pragma GCC diagnostic ignored "-Wmaybe-uninitialized" + #endif optional r; for (; i < minors_end; i++) { expr minor = args[i];