bug#3794: Several other problems in gdb-mi [RE: bug#3794: Error in json from gdb-ui]

[Nick Roberts]

 > 4. Killing a gdb buffer won't send the `detach' command to the gdb
 > process, leaving the debugged process permentally being stopped.  This
 > is often unconvenient.

I've reverted Dmitry's fix for this as detaching might not be what the user
wants and it can cause problems (bug#4375: can't kill killed gud buffer).

If you want to deatch the inferior you should do it manually with the GDB CLI
command "detach" before killing the GUD buffer.

-- 
Nick                                           http://www.inet.net.nz/~nickrob