Remove duplicate history entries in command buffer

[Pavel Sanda]

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.

Pavel