diff options
| author | Niklas Haas <github-c6e1c8@haasn.xyz> | 2016-08-14 08:18:32 +0200 |
|---|---|---|
| committer | Dave Davenport <DaveDavenport@users.noreply.github.com> | 2016-08-14 08:18:32 +0200 |
| commit | acdd8ddb5ae7c264d8dd29085368453e6f82cbce (patch) | |
| tree | d2a4bb81b81506df02e9674df59e8f8808c64f7e /script | |
| parent | b5595d7a7ec5182ae28da162191804641aa9b37f (diff) | |
Use bash instead of sh for get_git_rev.sh (#445)
The script relies on bash extensions to `echo`, which is not portable to
POSIX shells. Simplest fix is to request bash explicitly.
Diffstat (limited to 'script')
| -rwxr-xr-x | script/get_git_rev.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/script/get_git_rev.sh b/script/get_git_rev.sh index 5970e698..ee718d5e 100755 --- a/script/get_git_rev.sh +++ b/script/get_git_rev.sh @@ -1,4 +1,4 @@ -#!/usr/bin/env sh +#!/usr/bin/env bash DIR=$1 FILE=$2 |