Make `$HISTORY_IGNORE` have proper defaults and add `duplicates` to the manual
- Makes
$HISTORY_IGNORE
default to[ 'no_such_command', 'whitespace' 'duplicates' ]
. - Noted about `duplicates in the manual.
$HISTORY_IGNORE
default to [ 'no_such_command', 'whitespace' 'duplicates' ]
.