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 /install.sh | |
| 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
Diffstat (limited to 'install.sh')
0 files changed, 0 insertions, 0 deletions