Symbol: I386_IPI_DDB
sys/arch/i386/i386/db_mp.c
130
i386_send_ipi(cpu_info[cpu], I386_IPI_DDB);
sys/arch/i386/i386/db_mp.c
60
i386_send_ipi(cpu_info[i], I386_IPI_DDB);