# CONFIG_X86_32_NON_STANDARD is not set