Remove duplicate history entries in command buffer
Jean-Marc Lasgouttes
lasgouttes.lyx.org at free.fr
Sun Jul 10 17:42:49 UTC 2022
Le 10/07/2022 à 18:38, Kornel Benko a écrit :
> I don't get it.
> 1.) I like the rim(), was about to use it too ... but was unsure if sometimes
> one needs spaces at end.
In this case, I can remove it from both cases. It is not right to
maintain two lists and have one which is different from the other for no
reason. We can do what you prefer, but in sync.
> 2.) If I understand correctly, the your patch only omits repetition of the last command.
> But in the history there may be more of them
I am uneasy with the idea of removing stuff in the whole history because
it was used again. Maybe just because I am use dthe the 'ignoredups'
history control of bash, instead of 'erasedups'.
Moreover, the justification in your first message was only for the last
command, not for the older ones. But I am open for arguments on when it
is useful.
JMarc
More information about the lyx-devel
mailing list