Switch from bash to ksh, in the hope that more systems support it (one
report of a site without an available bash).