Hi Andrew.

Non-trivial in that I'm unsure of original intent but trivial in that 
it's just a printk()...

On bootup, I see:

pnp: the driver 'i8042 kbd' has been registered
pnp: match found with the PnP device '00:05' and the driver 'i8042 kbd'
pnp: the driver 'i8042 aux' has been registered
PNP: PS/2 controller doesn't have AUX irq; using default 0xc
PNP: PS/2 Controller [PNP0303] at 0x60,0x64 irq 112
serio: i8042 AUX port at 0x60,0x64 irq 12
serio: i8042 KBD port at 0x60,0x64 irq 1

That "irq 112" (last PNP: line) should read "irq 1,12" but is being run 
together:

printk(KERN_INFO "PNP: PS/2 Controller [%s%s%s] at %#x,%#x irq %d%s%d\n",
	i8042_pnp_kbd_name,
	(result_kbd > 0 && result_aux > 0) ? "," : "",
	i8042_pnp_aux_name,
	i8042_data_reg,
	i8042_command_reg,
	i8042_kbd_irq,
	(result_aux > 0) ? "," : "", i8042_aux_irq);

That first 'foo ? "," : ""' construct there seems somewhat okay-ish 
since i8042_pnp_aux_name is a 0-string when result_aux <= 0, but this 
obviously does not work for i8042_aux_irq (an integer).

In my case result_aux is 0 due to my BIOS not exporting a PS/2 mouse PNP 
id after which the code just assigns the default irq 12 (the first PNP: 
line above) but winds up printing "irq 112". Due to that default 
assignment, the correct fix would seem to be to just have "%d,%d". 
Attachment does this (and takes the opportunity to change two %#x format 
specifiers for the IRQs to %d).

Did not know who to more specifically bother about this; hope that's okay.

Rene.