Fix crack that formats an int into eight hex digits. Why the simple
sprintf() that originally was used here was not good enough, but had
to be replaced (in 2009) by broken and hard to understand code I have
no idea.

Found during link-time code generation (!).

Change-Id: I05b33ca0fcb6a47a846ec2ff294243c5639a5b49