Symbol: bebox_send_ipi
sys/arch/bebox/bebox/ipi_bebox.c
42
static void bebox_send_ipi(cpuid_t, uint32_t);
sys/arch/bebox/bebox/ipi_bebox.c
49
ipiops.ppc_send_ipi = bebox_send_ipi;