Converting bash vars to lowercase

Bash has a built-in way of converting variables to lower-case (as opposed to piping things through tr [:lower:] as I’ve done until now):

a="HELLO";
echo ${a,,};

That’s it, two commas do the trick.