[MI, doc] flush output in -gdb-exit

Eli Zaretskii eliz@gnu.org
Thu Dec 17 19:54:00 GMT 2009

> From: Vladimir Prus <vladimir@codesourcery.com>
> Date: Thu, 17 Dec 2009 10:46:03 +0300
> OK?

Yes, after this:

> +take some time for GDB to actually exit.  During that time, GDB
                      ^^^                                      ^^^

> +performs necessary cleanups, including killing programs being debugged
> +or disconnecting from debug hardware, so the frontend should wait till
> +GDB exits and should only forcibly kill GDB if it fails to exit in
   ^^^                                     ^^^

More information about the Gdb-patches mailing list