Index: kernel/genarch/src/drivers/i8259/i8259.c
===================================================================
--- kernel/genarch/src/drivers/i8259/i8259.c	(revision fd67c9f8dcdd34e9ee9ae504ae566e0d47cebb67)
+++ kernel/genarch/src/drivers/i8259/i8259.c	(revision 534bcdf6f87db58a9f44fa4244510aeed09d0c4e)
@@ -48,5 +48,5 @@
 
 void i8259_init(i8259_t *pic0, i8259_t *pic1, inr_t pic1_irq,
-    unsigned int irq0_int, unsigned int irq8_int)
+    unsigned int irq0_vec)
 {
 	saved_pic0 = pic0;
@@ -56,6 +56,6 @@
 	pio_write_8(&pic0->port1, PIC_ICW1 | PIC_ICW1_NEEDICW4);
 
-	/* ICW2: IRQ 0 maps to INT irq0_int */
-	pio_write_8(&pic0->port2, irq0_int);
+	/* ICW2: IRQ 0 maps to interrupt vector address irq0_vec */
+	pio_write_8(&pic0->port2, irq0_vec);
 
 	/* ICW3: pic1 using IRQ IRQ_PIC1 */
@@ -68,6 +68,6 @@
 	pio_write_8(&pic1->port1, PIC_ICW1 | PIC_ICW1_NEEDICW4);
 
-	/* ICW2: IRQ 8 maps to INT irq8_int */
-	pio_write_8(&pic1->port2, irq8_int);
+	/* ICW2: IRQ 8 maps to interrupt vector address irq0_vec + 8 */
+	pio_write_8(&pic1->port2, irq0_vec + PIC_IRQ_COUNT);
 
 	/* ICW3: pic1 is known as IRQ_PIC1 */