From ac90dba90fba4dc86d0733ac88fcf941ea36fe84 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 24 Sep 2018 08:41:07 -0700
Subject: [PATCH] chore(library/compiler/csimp): disable bogus warning

---
 src/library/compiler/csimp.cpp | 4 ++++
 1 file changed, 4 insertions(+)

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<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];