coverity: explicitly use bash instead of sh

On Ubuntu `/bin/sh` is a symlink to `/bin/dash`, which doesn't support
certain builtins used by the Coverity script (namely pushd/popd)
This commit is contained in:
Frantisek Sumsal 2019-11-05 21:49:39 +01:00 committed by Andrii Nakryiko
parent 91e4f27dd7
commit d7a137510a

View File

@ -1,4 +1,4 @@
#!/bin/sh
#!/bin/bash
# Taken from: https://scan.coverity.com/scripts/travisci_build_coverity_scan.sh
# Local changes are annotated with "#[local]"