Symbol: openpic_send_ipi
sys/arch/powerpc/pic/ipi_openpic.c
54
static void openpic_send_ipi(cpuid_t, uint32_t);
sys/arch/powerpc/pic/ipi_openpic.c
62
ipiops.ppc_send_ipi = openpic_send_ipi;