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 /Makefile.dev | |
| parent | 53319bdde6fc1f0bac8424cc6cfa6ff759914b1c (diff) | |
| parent | fc75c8ebf556a0f95c9f42e864dbac73090ecc6a (diff) | |
Merge PR #8627: [dune] [opam] Install `revision` file when building with Dune.
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 \ |