diff options
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; \ |