# CONFIG_PPC_PTDUMP is not set