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

[Pedro Alves <palves@redhat.com>]

On 06/09/2015 07:40 PM, Patrick Palka wrote:
> On Tue, Jun 9, 2015 at 2:10 PM, Pedro Alves <palves@redhat.com> wrote:
>> 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?
> 
> An "ignoredups" option currently seems not useful in GDB since we
> already have the empty-command shorthand for running the previous
> command again, which does not add to the history.  But if we ever make
> the empty-command shorthand toggle-able then an "ignoredups"
> equivalent could be useful when the shorthand is turned off.  I am
> actually thinking about implementing that too, since I do not like the
> shorthand very much and would like to be able to turn it off.  So I
> might as well implement "ignoredups" too.

Alright, sounds good.  I like the shorthand myself, but then
that's why these things have knobs.  :-)

Thanks,
Pedro Alves