diff options
| author | Théo Zimmermann | 2018-10-08 15:03:48 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-08 15:03:48 +0200 |
| commit | 9c25908a3a766e07ed8f6f396c9197b0f924e0f8 (patch) | |
| tree | fed35644b3afb26b9c376c040eb07eba1e6b9019 /dev | |
| parent | 53319bdde6fc1f0bac8424cc6cfa6ff759914b1c (diff) | |
| parent | fc75c8ebf556a0f95c9f42e864dbac73090ecc6a (diff) | |
Merge PR #8627: [dune] [opam] Install `revision` file when building with Dune.
Diffstat (limited to 'dev')
| -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 |