patch ping

Tom Tromey
2016-09-14T19:27:56Z

I was talking with a fellow Mozillian today and found out that this
patch was never reviewed:

https://sourceware.org/ml/gdb-patches/2015-05/msg00132.html

Ping.

Tom