# CONFIG_64BITS is not set