/* This file is generated automatically by configure */ #include <stdint.h>