[OpenBIOS] [PATCH] PPC64: Switch to 32-bit mode in interrupts