[FYI] 'maint' merged into 'branch-1.11'

Merge branch 'maint' into branch-1.11 * maint: info: allow user to inhibit creation/update of '${infodir}/dir' dejagnu: allow the package developer to extend site.exp * THANKS: Fix whitespace issue. deps: partially revert commit `v1.11-512-g551' dejagnu: ensure 'srcdir' is define

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

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