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
---
 Makefile.dev | 27 +--------------------------
 1 file changed, 1 insertion(+), 26 deletions(-)

(limited to 'Makefile.dev')

diff --git a/Makefile.dev b/Makefile.dev
index 82b81908ac..6a2a1b2101 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -34,33 +34,8 @@ dev/camlp5.dbg:
 revision:
 	$(SHOW)'CHECK revision'
 	$(HIDE)rm -f revision.new
-ifeq ($(CHECKEDOUT),svn)
 	$(HIDE)set -e; \
-        if test -x "`which svn`"; then \
-	  export LC_ALL=C;\
-	  svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision.new; \
-	  svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision.new; \
-	fi
-endif
-ifeq ($(CHECKEDOUT),gnuarch)
-	$(HIDE)set -e; \
-        if test -x "`which tla`"; then \
-	  LANG=C; export LANG; \
-	  tla tree-version  >  revision.new ; \
-	  tla tree-revision | sed -ne 's|.*--||p' >> revision.new ; \
-	fi
-endif
-ifeq ($(CHECKEDOUT),git)
-	$(HIDE)set -e; \
-	if test -x "`which git`"; then \
-	  LANG=C; export LANG; \
-	  GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \
-	  GIT_HOST=$$(hostname); \
-	  GIT_PATH=$$(pwd); \
-	  (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \
-	  (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \
-	fi
-endif
+	./dev/tools/make_git_revision.sh > revision.new
 	$(HIDE)set -e; \
 	if test -e revision.new; then \
           if test -e revision; then \
-- 
cgit v1.2.3