Comment by darrenf

Why even use awk rather than the shell's (well, bash's) builtin printf?

    $ printf '%d\n' "0005"
    5