summaryrefslogtreecommitdiff
path: root/Makefile.build
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build12
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; \