// This file lists names that have to be renamed from the
// GTK header files.