diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-31 19:52:28 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-31 19:52:28 +0000 |
| commit | 98231b971df2323c16fef638c0b3fd2ba8eab07f (patch) | |
| tree | 0b465e18f9ce4415a736def021feef575e8ae660 | |
| parent | 6f8b2daa91084885a9aac674ad01089425ce8b6e (diff) | |
Fix last commit about revision: I'm unsure about the role of "set -e",
but it probably works only if placed in front of the shell line
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11026 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/Makefile.build b/Makefile.build index b8033ad53..dd2caf8cd 100644 --- a/Makefile.build +++ b/Makefile.build @@ -765,10 +765,9 @@ $(foreach f,$(RECTYPESML),$(eval $(call rectypes-rules-template,$(f)))) revision: $(SHOW)'CHECK revision' - $(HIDE)set -e $(HIDE)rm -f revision.new ifeq ($(CHECKEDOUT),svn) - $(HIDE)\ + $(HIDE)set -e; \ if test -x "`which svn`"; then \ export LC_ALL=C;\ svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision.new; \ @@ -776,7 +775,7 @@ ifeq ($(CHECKEDOUT),svn) fi endif ifeq ($(CHECKEDOUT),gnuarch) - $(HIDE)\ + $(HIDE)set -e; \ if test -x "`which tla`"; then \ LANG=C; export LANG; \ tla tree-version > revision.new ; \ @@ -784,7 +783,7 @@ ifeq ($(CHECKEDOUT),gnuarch) fi endif ifeq ($(CHECKEDOUT),git) - $(HIDE)\ + $(HIDE)set -e; \ if test -x "`which git`"; then \ LANG=C; export LANG; \ GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \ @@ -794,7 +793,7 @@ ifeq ($(CHECKEDOUT),git) git log -1 | sed -ne '/^commit /s/^commit[[:space:]]\+\(.*\)/\1/p' >> revision.new; \ fi endif - $(HIDE)\ + $(HIDE)set -e; \ if test -e revision; then \ if test "`cat revision`" = "`cat revision.new`" ; then \ rm -f revision.new; \ |