dot/bashrc: Minor options tweaks.

Enable `**' wildcards and GNU-style errors; omit things beginning with a
space from the history.

diff --git a/dot/bashrc b/dot/bashrc
index e8bf6a477e4a9b251520cffb508fa611e374a7a0..17e18bb5af1d82706a8e70ca0334e6c3def9bf52 100644 (file)
--- a/dot/bashrc
+++ b/dot/bashrc
@@ -69,6 +69,8 @@ shopt -s cmdhist
 shopt -u dotglob
 shopt -s expand_aliases
 shopt -s extglob
 shopt -u dotglob
 shopt -s expand_aliases
 shopt -s extglob

+shopt -s globstar
+shopt -s gnu_errfmt

 shopt -s histappend
 shopt -s histreedit
 shopt -u histverify
 shopt -s histappend
 shopt -s histreedit
 shopt -u histverify


@@ -83,6 +85,8 @@ shopt -s promptvars
 shopt -u shift_verbose
 shopt -s sourcepath
 
 shopt -u shift_verbose
 shopt -s sourcepath
 

+HISTCONTROL=ignorespace:erasedups
+

 # --- Set the CDPATH ---
 #
 # CDPATH=~/src:/usr/src:/usr/lib:/usr/share
 # --- Set the CDPATH ---
 #
 # CDPATH=~/src:/usr/src:/usr/lib:/usr/share