Understanding and using the $RANDOM internal variable in Bash, including its open-source implementation