diff options
| author | Emilio Jesus Gallego Arias | 2018-10-02 16:26:18 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-03 13:18:33 +0200 |
| commit | fc75c8ebf556a0f95c9f42e864dbac73090ecc6a (patch) | |
| tree | 327c57309791e0606b6389c7482f6818a29c2d8d /dev/tools | |
| parent | 016f4a302090bcbb4ad47197dda2c60d6f598f6a (diff) | |
[dune] [opam] Install `revision` file when building with Dune.
Fixes #8621
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/make_git_revision.sh | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/dev/tools/make_git_revision.sh b/dev/tools/make_git_revision.sh new file mode 100755 index 0000000000..84982f89b9 --- /dev/null +++ b/dev/tools/make_git_revision.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +if [ -x `which git` ] && [ -d .git ] || git rev-parse --git-dir > /dev/null 2>&1 +then + export LANG=C + GIT_BRANCH=$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p') + GIT_HOST=$(hostname) + GIT_PATH=$(pwd) + echo "${GIT_HOST}:${GIT_PATH},${GIT_BRANCH}" + echo $(git log -1 --pretty='format:%H') +fi |