printf '<%06s>', 12;   # prints "<000012>"