diff -ru gnumach.original/linux/src/arch/i386/kernel/bios32.c gnumach.modificado/linux/src/arch/i386/kernel/bios32.c
--- gnumach.original/linux/src/arch/i386/kernel/bios32.c	2005-09-05 00:06:27.000000000 +0200
+++ gnumach.modificado/linux/src/arch/i386/kernel/bios32.c	2005-11-12 17:30:44.000000000 +0100
@@ -225,7 +225,7 @@
 		major_revision = (pack >> 8) & 0xff;
 		minor_revision = pack & 0xff;
 		if (present_status || (signature != PCI_SIGNATURE)) {
-			printk ("pcibios_init : %s : BIOS32 Service Directory says PCI BIOS is present,\n"
+			printk ("pcibios_init: %s : BIOS32 Service Directory says PCI BIOS is present,\n"
 				"	but PCI_BIOS_PRESENT subfunction fails with present status of 0x%x\n"
 				"	and signature of 0x%08lx (%c%c%c%c).  mail drew@Colorado.EDU\n",
 				(signature == PCI_SIGNATURE) ?  "WARNING" : "ERROR",
@@ -237,7 +237,7 @@
 				pcibios_entry = 0;
 		}
 		if (pcibios_entry) {
-			printk ("pcibios_init : PCI BIOS revision %x.%02x entry at 0x%lx\n",
+			printk ("pcibios_init: PCI BIOS revision %x.%02x entry at 0x%lx\n",
 				major_revision, minor_revision, pcibios_entry);
 			return 1;
 		}
@@ -891,18 +891,18 @@
 		if (sum != 0)
 			continue;
 		if (check->fields.revision != 0) {
-			printk("pcibios_init : unsupported revision %d at 0x%p, mail drew@colorado.edu\n",
+			printk("pcibios_init: unsupported revision %d at 0x%p, mail drew@colorado.edu\n",
 				check->fields.revision, check);
 			continue;
 		}
-		printk ("pcibios_init : BIOS32 Service Directory structure at 0x%p\n", check);
+		printk ("pcibios_init: BIOS32 Service Directory structure at 0x%p\n", check);
 		if (!bios32_entry) {
 			if (check->fields.entry >= 0x100000) {
 				printk("pcibios_init: entry in high memory, trying direct PCI access\n");
 				access_pci = check_direct_pci();
 			} else {
 				bios32_entry = check->fields.entry;
-				printk ("pcibios_init : BIOS32 Service Directory entry at 0x%lx\n", bios32_entry);
+				printk ("pcibios_init: BIOS32 Service Directory entry at 0x%lx\n", bios32_entry);
 				bios32_indirect.address = bios32_entry;
 			}
 		}
Sólo en gnumach.modificado/linux/src/arch/i386/kernel: bios32.c~