--- /dev/null
+/* Copyright (C) 2008 Free Software Foundation, Inc.
+
+ This file is part of GDB.
+
+ This program is free software; you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation; either version 3 of the License, or
+ (at your option) any later version.
+
+ This program is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with this program. If not, see <http://www.gnu.org/licenses/>. */
+
+/* The libdecnumber library, on which GDB depends, includes a header file
+ called gstdint.h instead of relying directly on stdint.h. GDB, on the
+ other hand, includes stdint.h directly, relying on the fact that gnulib
+ generates a copy if the system doesn't provide one or if it is missing
+ some features. Unfortunately, gstdint.h and stdint.h cannot be included
+ at the same time, which may happen when we include a file from
+ libdecnumber.
+
+ The purpose of this file is to override the libdecnumber/gstdint.h file
+ to use stdint.h instead. Thanks to the order of our include path,
+ files from the GDB source tree have precedence over files from our
+ dependencies. So the presence of this file will ensure that we
+ consistently use the same stdint.h file when compiling GDB source
+ files. */
+
+#include <stdint.h>