Re: [PATCH 3/3, doc RFA] gdbserver debug_printf+timestamps: main patch

[Eli Zaretskii <eliz@gnu.org>]

> From: Doug Evans <dje@google.com>
> Date: Fri, 17 Jan 2014 14:45:00 -0800
> cc: gdb-patches <gdb-patches@sourceware.org>
> 
> --- a/gdb/NEWS
> +++ b/gdb/NEWS
> @@ -3,6 +3,14 @@
>  
>  *** Changes since GDB 7.7
>  
> +* New features in the GDB remote stub, GDBserver
> +
> +  ** New option --debug-format=option1[,option2,...] allows one to add
> +     additional text to each debugging message.  At present only timestamps
> +     are supported: --debug-format=timestamps.

I stumbled on "debugging message".  Why not say "to each output"
instead?

> +The @option{--debug-format=option1[,option2,...]} option tells
> +@code{gdbserver} to include additional information in each line of
> +debugging output.  Possible options are:

Again, "each line of debugging output" is somewhat vague.  (Aren't
there multi-line outputs, and if so, will gdbserver indeed precede
each of these lines with a timestamp?)  I hope we can find something
more clear.  Also, an example will help here.

Also, a @cindex entry here would be nice.

> @@ -44342,6 +44374,24 @@ Instruct @code{gdbserver} to display remote protocol debug output.
>  This option is intended for @code{gdbserver} development and for bug reports to
>  the developers.
>  
> +@item --debug-format=option1@r{[},option2,...@r{]}
> +Instruct @code{gdbserver} to include extra information in each line
> +of debugging output.
> +
> +Possible options are:

Why is this described twice?  I suggest to describe once, and leave a
cross-reference in the second place.

The documentation part is OK with these fixed.

Thanks.