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

[Pedro Alves <palves@redhat.com>]

On 06/04/2015 05:21 PM, Patrick Palka wrote:
> This patch implements the new option "history remove-duplicates", which
> controls whether GDB should remove duplicate command-history entries
> (off by default).
> 
> The motivation for this option is to be able to reduce the prevalence of
> basic commands such as "up" and "down" in the history file.  These
> common commands crowd out more unique commands in the history file (when
> the history file has a fixed size), and they make navigation of the
> history file via ^P, ^N and ^R more inconvenient.
> 

Did you consider bash's erasedups and ignoredups?  Specifically,
this seems to implement something like erasedups, and I'm wondering
how you'd fit in ignoredups in this option's UI.  Might be good to
prepare for it with an enum instead, something like:

  "set history duplicates ignore|erase|leave"

WDYT?

(haven't looked at the patch yet)

Thanks,
Pedro Alves