Thanks,

I didn't know how that was being done! I will do it immediately.

Sincerely,

Anders Lindgren

On Wed, Nov 4, 2015 at 5:40 PM, Glenn Morris <rgm@gnu.org> wrote:

Anders Lindgren wrote:

> I just pushed a fix for this, see

Then please close the bug report, eg by mailing 21301-done@debbugs.