I don't know how to close a debbugs. I believe only a debbugs admin can do
that?

On Fri, Aug 21, 2015 at 11:30 AM martin rudalics <rudalics@gmx.at> wrote:

> > One more thing.. also this bug now needs to be closed, right?
>
> Please do that.
>
> > And also
> > referenced in that commit message.
>
> I'll do that.  Please remind me as soon as you see the commit in
> ChangeLog.2.
>
> martin
>
>