Fix a shell invocation

We use bash syntax in a few places. This only matters if /bin/sh is not
the same as /bin/bash. One place had missed this.