Stripping leading zeros with bash

I needed to strip leading zeros from a variable, and found the "#" modifier in the shell manual pages:

$ FOO=09

$ echo ${FOO#0}

9

The number of occurences of the value following the # indicates how many to strip, and can also be applied to ASCII characters:

$ FOO=AAB

$ echo ${FOO#AA}

B

This is some nifty stuff!