diff --git a/src/kernel/boot/platform/bios_ia32/keyboard.cpp b/src/kernel/boot/platform/bios_ia32/keyboard.cpp
index 095b2f929c..ed0838cc57 100644
--- a/src/kernel/boot/platform/bios_ia32/keyboard.cpp
+++ b/src/kernel/boot/platform/bios_ia32/keyboard.cpp
@@ -33,6 +33,14 @@ check_for_key(void)
 }
 
 
+extern "C" void
+clear_key_buffer(void)
+{
+	while (check_for_key() != 0)
+		;
+}
+
+
 extern "C" union key
 wait_for_key(void)
 {
diff --git a/src/kernel/boot/platform/bios_ia32/keyboard.h b/src/kernel/boot/platform/bios_ia32/keyboard.h
index 7978bdcd89..54ceeadcdf 100644
--- a/src/kernel/boot/platform/bios_ia32/keyboard.h
+++ b/src/kernel/boot/platform/bios_ia32/keyboard.h
@@ -26,6 +26,7 @@ union key {
 extern "C" {
 #endif
 
+extern void clear_key_buffer(void);
 extern union key wait_for_key(void);
 extern uint32 check_for_boot_keys(void);