Stripping leading zeros using bash substring removal only

Yet another way, although this requires the extglob functionality being enabled:

echo ${string/#+(0)/}

The following would remove all the leading 0s from the string:

$ string="000123456000"
$ echo "${string#"${string%%[!0]*}"}"
123456000

Saying "${string%%[!0]*}" would return the match after deleting the longest trailing portion of the string that satisifies [!0]* -- essentially returning the zeros at the beginning.

"${string#"${string%%[!0]*}"}" would remove the part returned by the above from the beginning of the string.


Alternatively, you could use shell arithmetic:

$ string="0000123456000"
$ echo $((10#$string))
123456000

Tags:

Bash