Re: [PATCH v5 32/44] x86: Fix up use of X86_32BIT_INIT and X86_64 options