Index: kernel/arch/amd64/src/cpu/cpu.c
===================================================================
--- kernel/arch/amd64/src/cpu/cpu.c	(revision b3f8fb771f871e7f2bb35ce9339717639e8f86d6)
+++ kernel/arch/amd64/src/cpu/cpu.c	(revision dfa7bac346297f7790a17cd7dd459c2644aba6ef)
@@ -125,5 +125,6 @@
 {
 	CPU->arch.tss = tss_p;
-	CPU->arch.tss->iomap_base = &CPU->arch.tss->iomap[0] - ((uint8_t *) CPU->arch.tss);
+	CPU->arch.tss->iomap_base = &CPU->arch.tss->iomap[0] -
+	    ((uint8_t *) CPU->arch.tss);
 	CPU->fpu_owner = NULL;
 }
@@ -140,5 +141,7 @@
 		 * Check for AMD processor.
 		 */
-		if (info.cpuid_ebx==AMD_CPUID_EBX && info.cpuid_ecx==AMD_CPUID_ECX && info.cpuid_edx==AMD_CPUID_EDX) {
+		if (info.cpuid_ebx == AMD_CPUID_EBX &&
+		    info.cpuid_ecx == AMD_CPUID_ECX &&
+		    info.cpuid_edx == AMD_CPUID_EDX) {
 			CPU->arch.vendor = VendorAMD;
 		}
@@ -147,12 +150,14 @@
 		 * Check for Intel processor.
 		 */		
-		if (info.cpuid_ebx==INTEL_CPUID_EBX && info.cpuid_ecx==INTEL_CPUID_ECX && info.cpuid_edx==INTEL_CPUID_EDX) {
+		if (info.cpuid_ebx == INTEL_CPUID_EBX &&
+		    info.cpuid_ecx == INTEL_CPUID_ECX &&
+		    info.cpuid_edx == INTEL_CPUID_EDX) {
 			CPU->arch.vendor = VendorIntel;
 		}
 				
 		cpuid(1, &info);
-		CPU->arch.family = (info.cpuid_eax>>8)&0xf;
-		CPU->arch.model = (info.cpuid_eax>>4)&0xf;
-		CPU->arch.stepping = (info.cpuid_eax>>0)&0xf;						
+		CPU->arch.family = (info.cpuid_eax >> 8) & 0xf;
+		CPU->arch.model = (info.cpuid_eax >> 4) & 0xf;
+		CPU->arch.stepping = (info.cpuid_eax >> 0) & 0xf;						
 	}
 }
@@ -161,6 +166,6 @@
 {
 	printf("cpu%d: (%s family=%d model=%d stepping=%d) %dMHz\n",
-		m->id, vendor_str[m->arch.vendor], m->arch.family, m->arch.model, m->arch.stepping,
-		m->frequency_mhz);
+	    m->id, vendor_str[m->arch.vendor], m->arch.family, m->arch.model,
+	    m->arch.stepping, m->frequency_mhz);
 }