Re: [PATCH] Fix GDB build when using --disable-gdbmi

Tom Tromey
2019-05-10T21:16:06Z

>>>>> "Simon" == Simon Marchi <simon.marchi@efficios.com> writes:

Simon> I tried this, and I prefer the result. WDYT?

Thanks for doing this. It looks good to me.

Tom