CI: Change ci_build.sh to use bash instead of sh.
commitcf3d1f130e50cf63da4bb1031771605f6f443b6a
authorJia Tan <jiat0218@gmail.com>
Fri, 24 Mar 2023 12:06:33 +0000 (24 20:06 +0800)
committerJia Tan <jiat0218@gmail.com>
Fri, 24 Mar 2023 12:06:33 +0000 (24 20:06 +0800)
tree75a76a0fa3be9086fef11e2de1ae877b3ad5031f
parentddfe164368e779c40d061aa4ccc376129e92f8e1
CI: Change ci_build.sh to use bash instead of sh.

This script is only meant to be run as part of the CI build/test process
on machines that are known to have bash (Ubuntu and MacOS). If this
assumption changes in the future, then the bash specific commands will
need to be replaced with a more portable option. For now, it is
convenient to use bash commands.
build-aux/ci_build.sh