From fc75c8ebf556a0f95c9f42e864dbac73090ecc6a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Oct 2018 16:26:18 +0200
Subject: [dune] [opam] Install `revision` file when building with Dune.

Fixes #8621
---
 dev/tools/make_git_revision.sh | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100755 dev/tools/make_git_revision.sh

(limited to 'dev')

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
-- 
cgit v1.2.3