Remove duplicate history entries in command buffer

[Jean-Marc Lasgouttes]

Le 12/07/2022 à 22:15, Pavel Sanda a écrit :
> On Mon, Jul 11, 2022 at 02:25:49PM +0200, Kornel Benko wrote:
>> Am Mon, 11 Jul 2022 13:37:31 +0200
>> schrieb Pavel Sanda <sanda at lyx.org>:
>>
>>> On Mon, Jul 11, 2022 at 10:53:23AM +0200, Kornel Benko wrote:
>>>> So the outcome may be a new preference?
>>>
>>> Please no.
>>>
>>> Pavel
>>
>> What is your preference?
> 
> I do not have strong opinion whether erasing from history or just not
> duplicating last command is a better option.
> 
> JMarc's point about storing proper order in older commands makes sense in linux
> shell history. In LyX I am not convinced, or rather I can't remember that I
> really used sequences of commands except of those which are actually wrapped by
> command-sequence lfun.
> 
> But no hard opinion, except that this minute detail does not deserve new
> lyx preference.

I won't complain more about removing from the whole history, but the 
original patch will need to be updated. I suspect that the two command 
lists should be unified.

JMarc