diff options
| author |  thutchin <thutchin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-25 15:57:04 +0000 |
|---|---|---|
| committer | thutchin <thutchin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-25 15:57:04 +0000 |
| commit | af3f7473aa09bfd535e6e584eec89c4a1ac8e672 (patch) | |
| tree | e501bae70ff954a0ff8844bcbf8b75052ce12e80 | |
| parent | 7ac0e45f0e4740c8a51bfcd9eb11bc953b412997 (diff) | |
In the git-specific part of Makefile.build, call to hostname gave option
--fqdn. Changed this to -f (which has the same behavior) so it will work on
Mac OS 10.6 Note: Previous versions of Mac OS 10 don't have this option. Most
BSD's don't either. Their default behavior is to output the FQDN where Linux
defaults to outputting the short name.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12810 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 3df2f2155..e855d906c 100644 --- a/Makefile.build +++ b/Makefile.build @@ -711,7 +711,7 @@ ifeq ($(CHECKEDOUT),git) 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_HOST=$$(hostname -f); \ GIT_PATH=$$(pwd); \ (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \ (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \ |