Fix an integer-type mismatch between %04x in a printf format string