Le vendredi 23 juin 2023 à 11:24, Marc Chantreux <m...@unistra.fr> a écrit :
> salut,
>
> > Enfin tant que ça marche...
>
>
> idéalement il faudrait comprendre pourquoi mais là j'ai vraiment pas le
> temps :(
>
C'est déjà bien sympa de m'avoir filé ta config... :-)
Ma confusion vient du fait que j'ai crus (à tors, je viens de vérifier, ce
n'est pas dit dans le manuel) que l'option APPEND_HISTORY est l'option par
défaut avec HISTFILE=nom_fichier.
Mais c'est faux, voici l'info exacte :
INC_APPEND_HISTORY
This option works like APPEND_HISTORY except that new history lines are
added to the $HISTFILE incrementally (as soon as they are entered), rather than
waiting until the shell exits. The file will still be periodically re-written
to trim it when the number of lines grows 20% beyond the value specified by
$SAVEHIST (see also the HIST_SAVE_BY_COPY option).
APPEND_HISTORY <D>
If this is set, zsh sessions will append their history list to the history
file, rather than replace it. Thus, multiple parallel zsh sessions will all
have the new entries from their history lists added to the history file, in the
order that they exit. The file will still be periodically re-written to trim it
when the number of lines grows 20% beyond the value specified by $SAVEHIST (see
also the HIST_SAVE_BY_COPY option).
Du coup je n'ai pas gardé l'option :
EXTENDED_HISTORY <C>
Save each command’s beginning timestamp (in seconds since the epoch) and
the duration (in seconds) to the history file. The format of this prefixed data
is:
‘: <beginning time>:<elapsed seconds>;<command>’.
Pas besoin de dater, surtout si c'est humainement lisible
HIST_FIND_NO_DUPS
When searching for history entries in the line editor, do not display
duplicates of a line previously found, even if the duplicates are not
contiguous.
Me semble redondant avec HIST_IGNORE_ALL_DUPS qui en cas de doublon supprime
l'existant et ne garde que le nouveau, du coup il ne saurait pas trouver de
doublon.
Cf.
https://zsh.sourceforge.io/Doc/Release/Options.html
