Re: [PATCH] Add option to remove duplicate command history entries

[Eli Zaretskii <eliz@gnu.org>]

> From: Patrick Palka <patrick@parcs.ath.cx>
> Cc: Patrick Palka <patrick@parcs.ath.cx>
> Date: Thu,  4 Jun 2015 12:21:58 -0400
> 
> This patch implements the new option "history remove-duplicates", which
> controls whether GDB should remove duplicate command-history entries
> (off by default).

Thanks.

> gdb/doc/ChangeLog:
> 
> 	* gdb.texinfo: Document the new option
> 	"history remove-duplicates".

This ChangeLog entry should name the node in which you made the
changes, as if it were a function (i.e., in parentheses).

> diff --git a/gdb/NEWS b/gdb/NEWS
> index bbfb55d..411be32 100644
> --- a/gdb/NEWS
> +++ b/gdb/NEWS
> @@ -123,6 +123,10 @@ show max-completions
>    to avoid generating large completion lists, the computation of
>    which can cause the debugger to become temporarily unresponsive.
>  
> +set history remove-duplicates
> +show history remove-duplicates
> +  Control the removal of duplicate history entries.

This part is OK.

> +@cindex remove duplicate history
> +@kindex set history remove-duplicates
> +@item set history remove-duplicates
> +@itemx set history remove-duplicates on
> +Remove duplicate history entries added during the current session.  Before a

Given the description below, this summary is slightly misleading,
IMO.  Why not simply

  Keep in history of CLI commands only one copy of each command.

> +entry it finds. This option is off by default.
                 ^^
Two spaces between sentences, please.

The documentation parts are okay with these fixed.