// Dummy header not provided by GCC, doesn't seem to be required