diff options
author | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
commit | 3e96002677226c0cdaa8f355938a76cfb37a722a (patch) | |
tree | 3ca96e142fdb68e464d2f5f403f315282b94f922 /Makefile.build | |
parent | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff) |
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'Makefile.build')
-rw-r--r-- | Makefile.build | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/Makefile.build b/Makefile.build index 4a7354e4..8af5be00 100644 --- a/Makefile.build +++ b/Makefile.build @@ -6,7 +6,7 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile.build 13324 2010-07-24 19:21:23Z glondu $ +# $Id: Makefile.build 13477 2010-09-30 16:50:00Z vgross $ # Makefile for Coq @@ -340,14 +340,6 @@ install-ide-info: $(MKDIR) $(FULLIDELIB) $(INSTALLLIB) ide/FAQ $(FULLIDELIB) -# IM files - -IMFILES=$(addprefix ide/uim/, coqide.scm coqide-rules.scm coqide-custom.scm) - -install-im: - $(INSTALLLIB) $(IMFILES) $(UIMSCRIPTDIR) - uim-module-manager --register coqide - ########################################################################### # tests ########################################################################### @@ -716,7 +708,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; \ |