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.
>