printf format bugfix (hidden on 32-bit).