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

[Eli Zaretskii]

> 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
                      ^^^                                      ^^^
@value{GDBN}

> +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
   ^^^                                     ^^^
Likewise.