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