/* Dummy "stdint.h". */

#include <inttypes.h>