diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-31 19:06:22 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-31 19:06:22 +0000 |
| commit | 6f8b2daa91084885a9aac674ad01089425ce8b6e (patch) | |
| tree | d1a1e90a1c1e1ba1616a8069eebe9cb186dc51af | |
| parent | f350cd8cb53e675a5793336b9b17c4749fa474b8 (diff) | |
Attempt to avoid killing+recreating the file revision with same content.
This should prevent some useless coqtop+theories recompilation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11025 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 38 |
1 files changed, 24 insertions, 14 deletions
diff --git a/Makefile.build b/Makefile.build index 6577d0d0d..b8033ad53 100644 --- a/Makefile.build +++ b/Makefile.build @@ -764,36 +764,46 @@ $(foreach f,$(RECTYPESML),$(eval $(call rectypes-rules-template,$(f)))) .PHONY: revision revision: + $(SHOW)'CHECK revision' + $(HIDE)set -e + $(HIDE)rm -f revision.new ifeq ($(CHECKEDOUT),svn) - rm -f revision - set -e; \ - if test -x "`which svn`"; then \ + $(HIDE)\ + if test -x "`which svn`"; then \ export LC_ALL=C;\ - svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision; \ - svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision; \ + 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) - rm -f revision - set -e; \ - if test -x "`which tla`"; then \ + $(HIDE)\ + if test -x "`which tla`"; then \ LANG=C; export LANG; \ - tla tree-version > revision ; \ - tla tree-revision | sed -ne 's|.*--||p' >> revision ; \ + tla tree-version > revision.new ; \ + tla tree-revision | sed -ne 's|.*--||p' >> revision.new ; \ fi endif ifeq ($(CHECKEDOUT),git) - rm -f revision - set -e; \ + $(HIDE)\ if test -x "`which git`"; then \ LANG=C; export LANG; \ GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \ GIT_HOST=$$(hostname --fqdn); \ GIT_PATH=$$(pwd); \ - (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision; \ - git log -1 | sed -ne '/^commit /s/^commit[[:space:]]\+\(.*\)/\1/p' >> revision; \ + (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \ + git log -1 | sed -ne '/^commit /s/^commit[[:space:]]\+\(.*\)/\1/p' >> revision.new; \ fi endif + $(HIDE)\ + if test -e revision; then \ + if test "`cat revision`" = "`cat revision.new`" ; then \ + rm -f revision.new; \ + else \ + mv -f revision.new revision; \ + fi; \ + else \ + mv -f revision.new revision; \ + fi ########################################################################### # Default rules |