Merge PR #8627: [dune] [opam] Install `revision` file when building with Dune.

5 files changed, 24 insertions, 40 deletions

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 51fc2b035c..412bed8334 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -9,6 +9,7 @@
 ########## Build system ##########
 
 /Makefile*        @gares
+/dev/tools/make_git_revision.sh @gares
 
 /configure*       @ejgallego
 
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 \
diff --git a/configure.ml b/configure.ml
index a508ac6071..7cc58a3506 100644
--- a/configure.ml
+++ b/configure.ml
@@ -525,22 +525,10 @@ let arch_is_win32 = (arch = "win32")
 let exe = exe := if arch_is_win32 then ".exe" else ""; !exe
 let dll = if os_type_win32 then ".dll" else ".so"
 
-(** * VCS
-
-    Is the source tree checked out from a recognised
-    Version Control System ? *)
-
-let vcs =
-  let git_dir = try Sys.getenv "GIT_DIR" with Not_found -> ".git" in
-  if Sys.file_exists git_dir then "git"
-  else if Sys.file_exists ".svn/entries" then "svn"
-  else if dir_exists "{arch}" then "gnuarch"
-  else "none"
-
 (** * Git Precommit Hook *)
 let _ =
   let f = ".git/hooks/pre-commit" in
-  if vcs = "git" && dir_exists ".git/hooks" && not (Sys.file_exists f) then begin
+  if dir_exists ".git/hooks" && not (Sys.file_exists f) then begin
     cprintf "Creating pre-commit hook in %s" f;
     let o = open_out f in
     let pr s = fprintf o s in
@@ -1341,7 +1329,6 @@ let write_makefile f =
   pr "IDECDEPSFLAGS=%s\n" !idecdepsflags;
   pr "IDEINT=%s\n\n" !idearchdef;
   pr "# Defining REVISION\n";
-  pr "CHECKEDOUT=%s\n\n" vcs;
   pr "# Option to control compilation and installation of the documentation\n";
   pr "WITHDOC=%s\n\n" (if !prefs.withdoc then "all" else "no");
   pr "# Option to produce precompiled files for native_compute\n";
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
diff --git a/dune b/dune
index b758fc7b56..27c5e972fe 100644
--- a/dune
+++ b/dune
@@ -9,3 +9,13 @@
  (name vodeps)
  (deps tools/coq_dune.exe .vfiles.d))
   ; (action (run coq_dune .vfiles.d))))
+
+(install
+ (section lib)
+ (files
+   revision))
+
+(rule
+ (targets revision)
+ (deps (:rev-script dev/tools/make_git_revision.sh))
+ (action (with-stdout-to revision (run %{rev-script}))))