From d0582b253724d8836bb4c0a354e9f2d2d87f85fb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 May 2015 10:04:38 -0700
Subject: [PATCH] fix(library/user_recursors): warning

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

diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp
index e7148f2bf..c6fa8c135 100644
--- a/src/library/user_recursors.cpp
+++ b/src/library/user_recursors.cpp
@@ -94,6 +94,10 @@ recursor_info mk_recursor_info(environment const & env, name const & r) {
     if (!is_sort(C_rtype) || C_tele.size() != C_args.size()) {
         throw_invalid_motive(C);
     }
+    // The following pragma is for avoiding gcc bogus warning
+    #if defined(__GNUC__) && !defined(__CLANG__)
+    #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
+    #endif
     optional<unsigned> C_univ_pos;
     level C_lvl = sort_level(C_rtype);
     if (!is_standard(env) || !is_zero(C_lvl)) {