Index: kernel/arch/arm32/src/mach/raspberrypi/raspberrypi.c
===================================================================
--- kernel/arch/arm32/src/mach/raspberrypi/raspberrypi.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
+++ kernel/arch/arm32/src/mach/raspberrypi/raspberrypi.c	(revision e7c4115de0a5bf1dd17b4e273352cc4607d67e03)
@@ -50,5 +50,4 @@
 #include <interrupt.h>
 #include <ddi/ddi.h>
-#include <ddi/device.h>
 
 #define RPI_DEFAULT_MEMORY_START	0
@@ -118,5 +117,4 @@
 	static irq_t timer_irq;
 	irq_initialize(&timer_irq);
-	timer_irq.devno = device_assign_devno();
 	timer_irq.inr = BCM2835_TIMER1_IRQ;
 	timer_irq.claim = raspberrypi_timer_irq_claim;