On Wed, Feb 21, 2018 at 10:17:33PM -0500, Thompson, David wrote:
> Pushed.  Do I have to do something special to close this ticket?

I'm closing it by appending -done to the bug number in the email
address.