On Feb 14, 2017 12:40 PM, "Vibhav Pant" <vibhavp@gmail.com> wrote:

On Tue, Feb 14, 2017 at 9:17 PM, Tino Calancha <tino.calancha@gmail.com>
wrote:
> Thank you very much for your fast action.
> I have tested your patch and fix the problem.
> By the way, thanks for implementing the switch: it's a nice job.

Thanks, I've pushed the fix to master (how does one close bugs in debbugs?).


One way is to reply to NNNNN-done@debbugs.gnu.org, as I have done. Thanks
for the fix!