Mailing-list: contact zsh-users-help@xxxxxxx; run by ezmlm
What is the proper way to delete entries in the history?
Just load the history file in an editor, deleting things and save it?
I didn't dare as I was afraid to interfere with the zsh shell managing
the history file.