Note that configure.sh still uses the bashism $(RANDOM).
Change-Id: Ieebea089095d9073b3a94932791099f614ce120c