From af3f7473aa09bfd535e6e584eec89c4a1ac8e672 Mon Sep 17 00:00:00 2001
From: thutchin
Date: Thu, 25 Feb 2010 15:57:04 +0000
Subject: 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
---
 Makefile.build | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile.build b/Makefile.build
index 3df2f21551..e855d906cb 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; \
-- 
cgit v1.2.3