Chris Webster <chris@xxxxxxxxxxxx> writes: >> I suspect that we are already depend on <<< Bash-ism, so one more >> dependency to Bash-ism is not a problem here? I dunno. > > While GitHub could probably allow other shells to be used, changing > the default would probably break a lot of things at this point. Do we specifically ask for bash in our .github/ files? That would be perfectly acceptable. Then we only have to worry about their withdrawing support for bash which would never happen ;-) Thanks.