/* This file is not needed, but in practice gdb might try to include it.  */