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 /Makefile.dev | |
| parent | 016f4a302090bcbb4ad47197dda2c60d6f598f6a (diff) | |
[dune] [opam] Install `revision` file when building with Dune.
Fixes #8621
Diffstat (limited to 'Makefile.dev')
| -rw-r--r-- | Makefile.dev | 27 |
1 files changed, 1 insertions, 26 deletions
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 \ |