diff options
| author | Benoit GALATI <benoit.galati@gmail.com> | 2020-05-21 18:29:00 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-21 18:29:00 +0200 |
| commit | fcd0747bc123d2c0775f8d757f0135067905ac0d (patch) | |
| tree | 41bac14e9fcf107f790df5ababaa36ee835d7951 /lib/history.zsh | |
| parent | d8f674cc8e4a3139db6bd10ea28a27e36aab0088 (diff) | |
| download | zsh-fcd0747bc123d2c0775f8d757f0135067905ac0d.tar.gz zsh-fcd0747bc123d2c0775f8d757f0135067905ac0d.tar.bz2 zsh-fcd0747bc123d2c0775f8d757f0135067905ac0d.zip | |
core: remove inc_append_history option (#8048)
Diffstat (limited to 'lib/history.zsh')
| -rw-r--r-- | lib/history.zsh | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/history.zsh b/lib/history.zsh index 52e45bf4c..0f04de215 100644 --- a/lib/history.zsh +++ b/lib/history.zsh @@ -36,5 +36,4 @@ setopt hist_expire_dups_first # delete duplicates first when HISTFILE size excee setopt hist_ignore_dups # ignore duplicated commands history list setopt hist_ignore_space # ignore commands that start with space setopt hist_verify # show command with history expansion to user before running it -setopt inc_append_history # add commands to HISTFILE in order of execution setopt share_history # share command history data |