The local man pages intalled in /usr/local/share/man should be checked
before the system's man pages for matches, since the tools installed in
/usr/local/bin have precedence over the ones at /bin and /usr/bin.
Change bash history management to ignore consecutive duplicates and
commands starting with a whitespace.
