Re: [OpenBIOS] [PATCH, RFC] ppc: Turn 32-bit ppc64 into a config option, to be deprecated