Subject: Re: bug#9773: "make install-info" with DESTDIR writes unwanted usr/share/info/dir.gz

From: Stefano Lattarini <[email-masked]>
Date: Sat, 29 Oct 2011 12:32:04 +0200

tags 9773 patch
close 9773
thanks

On Sunday 23 October 2011, Stefano Lattarini wrote:
> Here is my proposed patch (for maint).  I will push in 72 hours
> if there is no objection or review by then.
> 
I've pushed the patch to maint now (after addressing the nits
pointed out by Jonathan).  I'm thus closing this report.

Regards,
  Stefano