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

[Vladimir Prus <vladimir@codesourcery.com>]

I've noticed that under frontend, -gdb-exit may "timeout", even though it sends "^exit"
immediately. There was a flush missing. This patch adds it, and clarifies that frontend
should wait for GDB to actually exit, not just acknoledge the request.

OK?

- Volodya

diff --git a/gdb/doc/gdb.texinfo b/gdb/doc/gdb.texinfo
index e880838..1824a6c 100644
--- a/gdb/doc/gdb.texinfo
+++ b/gdb/doc/gdb.texinfo
@@ -21955,6 +21955,13 @@ Quitting @value{GDBN} just prints the result class @samp{^exit}.
 <- ^exit
 @end smallexample

+Please note that @samp{^exit} is printed immediately, but it might
+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
+reasonable time.
+
 @subheading A Bad Command

 Here's what happens if you pass a non-existent command:
diff --git a/gdb/mi/mi-main.c b/gdb/mi/mi-main.c
index 2332752..0c8e917 100644
--- a/gdb/mi/mi-main.c
+++ b/gdb/mi/mi-main.c
@@ -111,6 +111,7 @@ mi_cmd_gdb_exit (char *command, char **argv, int argc)
     fputs_unfiltered (current_token, raw_stdout);
   fputs_unfiltered ("^exit\n", raw_stdout);
   mi_out_put (uiout, raw_stdout);
+  gdb_flush (raw_stdout);
   /* FIXME: The function called is not yet a formal libgdb function.  */
   quit_force (NULL, FROM_TTY);
 }

- Volodya