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