Subject: Re: bug#13304: ping
From: Dima Kogan <[email-masked]>
To: Eli Zaretskii <[email-masked]>
Cc: [email-masked]
Date: Mon, 21 Sep 2015 11:38:16 -0700
List-Id: <debbugs-submit.debbugs.gnu.org>

Eli Zaretskii <[email-masked]> writes:

> Thanks, pushed.
>
> Should we close the bug now?

Thanks for doing that. You accidentally pushed the original patch, the
one from before I addressed Michael's comments, so it might be good to
update the tree with the later patch. In any case, I'm closing the bug.
Thanks again.