/trunk/kernel/generic/src/ddi/device.c |
---|
34,6 → 34,7 |
* @brief Device numbers. |
*/ |
#include <arch/types.h> |
#include <ddi/device.h> |
#include <atomic.h> |
#include <debug.h> |
/trunk/kernel/arch/ppc32/src/interrupt.c |
---|
80,18 → 80,5 |
exc_register(VECTOR_DECREMENTER, "timer", exception_decrementer); |
} |
static void ipc_int(int n, istate_t *istate) |
{ |
ipc_irq_send_notif(n - INT_OFFSET); |
} |
/* Reregister irq to be IPC-ready */ |
void irq_ipc_bind_arch(unative_t irq) |
{ |
int_register(irq, "ipc_int", ipc_int); |
} |
/** @} |
*/ |