# CONFIG_MPIC_MSGR is not set