2 files changed, 3 insertions, 17 deletions
diff --git a/src/arch/i386/include/ipxe/bios_timer.h b/src/arch/i386/include/ipxe/bios_timer.h
index f9fc80412..407780a6a 100644
--- a/src/arch/i386/include/ipxe/bios_timer.h
+++ b/src/arch/i386/include/ipxe/bios_timer.h
@@ -15,7 +15,7 @@ FILE_LICENCE ( GPL2_OR_LATER );
 #define TIMER_PREFIX_pcbios __pcbios_
 #endif
 
-#include <ipxe/timer2.h>
+#include <ipxe/pit8254.h>
 
 /**
  * Delay for a fixed number of microseconds
@@ -25,9 +25,9 @@ FILE_LICENCE ( GPL2_OR_LATER );
 static inline __always_inline void
 TIMER_INLINE ( pcbios, udelay ) ( unsigned long usecs ) {
 	/* BIOS timer is not high-resolution enough for udelay(), so
-	 * we use timer2
+	 * we use the 8254 Programmable Interval Timer.
 	 */
-	timer2_udelay ( usecs );
+	pit8254_udelay ( usecs );
 }
 
 /**
diff --git a/src/arch/i386/include/ipxe/timer2.h b/src/arch/i386/include/ipxe/timer2.h
deleted file mode 100644
index 322a3ed59..000000000
--- a/src/arch/i386/include/ipxe/timer2.h
+++ /dev/null
@@ -1,14 +0,0 @@
-#ifndef _IPXE_TIMER2_H
-#define _IPXE_TIMER2_H
-
-/** @file
- *
- * Timer chip control
- *
- */
-
-FILE_LICENCE ( GPL2_OR_LATER );
-
-extern void timer2_udelay ( unsigned long usecs );
-
-#endif /* _IPXE_TIMER2_H */