diff --git a/maintenance/gen_deps.sh b/maintenance/gen_deps.sh index 2bce0cf493b..6191afa90b7 100755 --- a/maintenance/gen_deps.sh +++ b/maintenance/gen_deps.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/bin/sh set -e -o pipefail maintenance_dir="$(realpath $(dirname $0))" [ "$(which dune-deps)" != '' ] || (echo 'missing required executable "dune-deps"; try `opam install dune-deps`' && exit 1)