Shell Programming and Scripting

Say I have a number x=123, but I want to it be x=000123, because I need to use it in as a file name. thanks!

In bash

Code:

y=$(printf "%06d" 13)

will result in 000013 assigned to y. I'd not recommend maintaining your value this way, but use printf to format your filename with whatever inputs are necessary and converting the value at that time. Something like this:

Code:

fname="$( printf "%s/foo%06d.%s" $directory $x $ext )"

or something similar.

If you are willing to use Ksh instead of bash, use the typeset command and each time the variable is used it will be presented with the format you desire:

Code:

$ typeset -Z6 x      # -Zn is right justify to a field size of n, pad w/ zeros
$ x=26
$ echo $x
000026

This seems much cleaner to me, but it seems unsupported in bash.

thanks a lot!