gdb-disable-makeinfo.patch

diff --git a/configure b/configure
index 64d287d..ae1d2b8 100755
--- a/configure
+++ b/configure
@@ -8038,21 +8038,26 @@ fi
 done
 test -n "$MAKEINFO" || MAKEINFO="$MISSING makeinfo"
 
-case " $build_configdirs " in
-  *" texinfo "*) MAKEINFO='$$r/$(BUILD_SUBDIR)/texinfo/makeinfo/makeinfo' ;;
-  *)
+if test "${MAKEINFO}" = "true"; then
+  # Disable makeinfo if requested
+  MAKEINFO=true
+else
+  case " $build_configdirs " in
+    *" texinfo "*) MAKEINFO='$$r/$(BUILD_SUBDIR)/texinfo/makeinfo/makeinfo' ;;
+    *)
 
-    # For an installed makeinfo, we require it to be from texinfo 4.7 or
-    # higher, else we use the "missing" dummy.
-    if ${MAKEINFO} --version \
-       | egrep 'texinfo[^0-9]*(4\.([7-9]|[1-9][0-9])|[5-9]|[1-9][0-9])' >/dev/null 2>&1; then
-      :
-    else
-      MAKEINFO="$MISSING makeinfo"
-    fi
-    ;;
+      # For an installed makeinfo, we require it to be from texinfo 4.7 or
+      # higher, else we use the "missing" dummy.
+      if ${MAKEINFO} --version \
+         | egrep 'texinfo[^0-9]*(4\.([7-9]|[1-9][0-9])|[5-9]|[1-9][0-9])' >/dev/null 2>&1; then
+        :
+      else
+        MAKEINFO="$MISSING makeinfo"
+      fi
+      ;;
 
-esac
+  esac
+fi
 
 # FIXME: expect and dejagnu may become build tools?