diff --git a/src/kernel/boot/platform/bios_ia32/start.c b/src/kernel/boot/platform/bios_ia32/start.c
index d245f44221..493b0dc7d0 100644
--- a/src/kernel/boot/platform/bios_ia32/start.c
+++ b/src/kernel/boot/platform/bios_ia32/start.c
@@ -56,7 +56,7 @@ void
 platform_start_kernel(void)
 {
 	mmu_init_for_kernel();
-	printf("kernel args at %p\n", &gKernelArgs);
+	printf("kernel entry at %lx\n", gKernelEntry);
 
 	asm("movl	%0, %%eax;	"			// move stack out of way
 		"movl	%%eax, %%esp; "