Remove duplicate history entries in command buffer

[Jean-Marc Lasgouttes]

Le 13/07/2022 à 17:49, Kornel Benko a écrit :
> Works nice. As expected, only the newly entered command is made uniq.
> 
> IMHO this should go in.

Thanks. This is in now.

JMarc