fix(BASH_COMPLETION_USER_FILE): explicitly check if it is not /dev/null

Users often set `BASH_COMPLETION_USER_FILE=/dev/null' to explicitly
express that there is no user configuration file.  However, in broken
systems, /dev/null may be a regular file that contains random outputs
from arbitary commands whose outputs are discarded.  We shall
explicitly confirm that the path is not `/dev/null' before sourcing
because we do not want to source this unexpected `/dev/null' file.

In fact, this caused a problem in the CI testing on GitHub [1] where
the command history is output to `HISTFILE=/dev/null'.  Here,
`/dev/null' gets the history entry `source bash_completion' and then
sourced from `bash_completion' itself, which results in an infinite
source chain of `bash_completion' -> `/dev/null' -> `bash_completion'
-> `/dev/null' -> ... while invoking random commands from the command
history.

[1] scop#529

Author: akinomyoga

bash_completion

@@ -2369,8 +2369,12 @@ fi
 unset compat_dir i _blacklist_glob
 
 # source user completion file
+#
+# Remark: We explicitly check that $user_completion is not '/dev/null' since
+#   /dev/null may be a regular file in broken systems and can contain arbitrary
+#   garbages of suppressed command outputs.
 user_completion=${BASH_COMPLETION_USER_FILE:-~/.bash_completion}
-[[ ${BASH_SOURCE[0]} != "$user_completion" && -r $user_completion && -f $user_completion ]] &&
+[[ $user_completion != "${BASH_SOURCE[0]}" && $user_completion != /dev/null && -r $user_completion && -f $user_completion ]] &&
     . $user_completion
 unset user_completion