Symbol: PPC_IPI_DDB
sys/arch/macppc/dev/openpic.c
741
case PPC_IPI_DDB:
sys/arch/powerpc/ddb/db_interface.c
129
ppc_send_ipi(&cpu_info[i], PPC_IPI_DDB);
sys/arch/powerpc/ddb/db_interface.c
327
ppc_send_ipi(&cpu_info[cpu], PPC_IPI_DDB);