diff options
| author | lmamane | 2009-02-11 09:28:26 +0000 |
|---|---|---|
| committer | lmamane | 2009-02-11 09:28:26 +0000 |
| commit | 1b7b14ab1d0683fc053c635a7db98941bdf89ab9 (patch) | |
| tree | 9b423cdc1a98266f90332ac87b8cf5dd421c6e09 | |
| parent | 038266740f02b6691d9072466e38762133ca0736 (diff) | |
config/revision.ml, git: handle case when not at tip of a branch
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11910 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 562228f853..a7442c457f 100644 --- a/Makefile.build +++ b/Makefile.build @@ -807,7 +807,7 @@ ifeq ($(CHECKEDOUT),git) GIT_HOST=$$(hostname --fqdn); \ GIT_PATH=$$(pwd); \ echo "let version = \"$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}\"" > revision.new; \ - echo "let revision = \"$$(git show-ref $${GIT_BRANCH}|sed -ne 's/ .*//p')\"" >> revision.new; \ + echo "let revision = \"$$(git log -1 --pretty='format:%H')\"" >> revision.new; \ fi endif $(HIDE)set -e; \ |