diff -r 534d3716bbbe xen/arch/x86/cpu/mcheck/mce.c
--- a/xen/arch/x86/cpu/mcheck/mce.c	Tue Jul 21 12:06:52 2009 +0100
+++ b/xen/arch/x86/cpu/mcheck/mce.c	Tue Jul 21 16:56:07 2009 +0200
@@ -798,7 +798,7 @@ int mce_wrmsr(u32 msr, u64 value)
     case MSR_IA32_MCG_CTL:
         if ( value && (value + 1) )
         {
-            gdprintk(XENLOG_WARNING, "MCE: value written to MCG_CTL"
+            gdprintk(XENLOG_WARNING, "MCE: value written to MCG_CTL "
                      "should be all 0s or 1s\n");
             ret = -1;
             break;
@@ -847,7 +847,7 @@ int mce_wrmsr(u32 msr, u64 value)
         case MSR_IA32_MC0_CTL:
             if ( value && (value + 1) )
             {
-                gdprintk(XENLOG_WARNING, "MCE: value written to MC%u_CTL"
+                gdprintk(XENLOG_WARNING, "MCE: value written to MC%u_CTL "
                          "should be all 0s or 1s (is %"PRIx64")\n",
                          bank, value);
                 ret = -1;