--- /dev/null
+/* This header is only for use of libdecnumber built as part of
+ libgcc. The targets supported for decimal floating point have
+ <stdint.h>; libdecnumber uses GCC_HEADER_STDINT only for the sake
+ of the host. */
+
+#include <stdint.h>