diff -r 57033bc8cd30 xen/arch/x86/cpu/mcheck/mce.c
--- a/xen/arch/x86/cpu/mcheck/mce.c	Fri Aug 07 17:31:27 2009 +0100
+++ b/xen/arch/x86/cpu/mcheck/mce.c	Mon Aug 10 11:48:06 2009 +0200
@@ -798,8 +798,8 @@ 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 "
-                     "should be all 0s or 1s\n");
+            gdprintk(XENLOG_WARNING, "MCE: value \"%"PRIx64"\" written "
+                     "to MCG_CTL should be all 0s or 1s\n", value);
             ret = -1;
             break;
         }