Re: [PATCH v3 2/3] GDBServer: introduce --server-output command line option

[Eli Zaretskii <eliz@gnu.org>]

> From: Cleber Rosa <crosa@redhat.com>
> Cc: areis@redhat.com, Cleber Rosa <crosa@redhat.com>
> Date: Tue, 31 Mar 2015 12:49:06 -0300
> 
> This command line option will redirect all of the gdbserver's own
> output (always sent to stderr) to a separate file.  This feature makes
> it possible to distinguish between the inferior process stderr and
> gdbserver's own stderr.  Example use case:
> 
>  $ gdbserver --server-output=log :2222 bin >bin.out 2>bin.err
> 
> Server output will be sent to file named "log", and the inferior
> output and error messages will be on files "bin.out" and "bin.err",
> respectively.
> 
> gdb/Changelog:
> 2015-03-31  Cleber Rosa  <crosa@redhat.com>
> 
> 	* NEWS: New feature in the GDBserver: --server-output.
> 
> gdb/doc/ChangeLog:
> 2015-03-31  Cleber Rosa  <crosa@redhat.com>
> 
> 	* gdb.texinfo (info): Added section on command line and monitor
> 	commands.
> 	(gdbserver man): Added section on new command line option.
> 
> gdb/gdbserver/ChangeLog:
> 2015-03-31  Cleber Rosa  <crosa@redhat.com>
> 
> 	* server.c (set_server_output): New utility function.
> 	(gdbserver_usage): Add help on '--server-output' option.
> 	(captured_main): Add command line option parsing for
> 	'--server-output'.

OK for the documentation parts.

Thanks.