Here is a patch:

From: Santiago Vila <sanv...@debian.org>
Subject: Modify doc/Makefile.in to avoid /usr/share/info/dir.gz.

--- a/doc/Makefile.in
+++ b/doc/Makefile.in
@@ -773,8 +773,7 @@
          echo " $(INSTALL_DATA) $$files '$(DESTDIR)$(infodir)'"; \
          $(INSTALL_DATA) $$files "$(DESTDIR)$(infodir)" || exit $$?; done
        @$(POST_INSTALL)
-       @if (install-info --version && \
-            install-info --version 2>&1 | sed 1q | grep -i -v debian) 
>/dev/null 2>&1; then \
+       @if false; then \
          list='$(INFO_DEPS)'; test -n "$(infodir)" || list=; \
          for file in $$list; do \
            relfile=`echo "$$file" | sed 's|^.*/||'`; \

Reply via email to