Remove duplicate history entries in command buffer

[Jean-Marc Lasgouttes]

Le 12/07/2022 à 22:19, Jean-Marc Lasgouttes a écrit :
> 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.

I just discovered that the sexy and fast way of removing a string from a 
vector of strings is the erase-remove idiom:
https://en.wikipedia.org/wiki/Erase%E2%80%93remove_idiom

JMarc