HelenOS sources

BCM2835_TIMER1_IRQ  119 kernel/arch/arm32/src/mach/raspberrypi/raspberrypi.c 	timer_irq.inr = BCM2835_TIMER1_IRQ;
BCM2835_TIMER1_IRQ  124 kernel/arch/arm32/src/mach/raspberrypi/raspberrypi.c 	bcm2835_irc_enable(raspi.irc, BCM2835_TIMER1_IRQ);