November 28, 2013
	long x = 0x123456789;
	writef("%0x",x);

prints 123456789

Seems like it has enough info to fill out to 16 hex digits...