From d7a137510af89c7ca0cec0cb35bb63adbf0901f9 Mon Sep 17 00:00:00 2001
From: Frantisek Sumsal <frantisek@sumsal.cz>
Date: Tue, 5 Nov 2019 21:49:39 +0100
Subject: [PATCH] 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)
---
 scripts/coverity.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/coverity.sh b/scripts/coverity.sh
index b17d814..99e4809 100755
--- a/scripts/coverity.sh
+++ b/scripts/coverity.sh
@@ -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]"