#! /bin/sh
#
# Some of these should really be done by man2html
#
# The ~/xxx links don't really work -- netscape doesn't expand the home
# directory of the user running navigator
#
sed -e 's|gnu.bash.bug|gnu.bash.bug|g' \
-e 's|/bin/bash|/bin/bash|g' \
-e 's|/etc/profile|/etc/profile|g' \
-e 's|~/.bash_profile|~/.bash_profile|g' \
-e 's|~/.bash_login|~/.bash_login|g' \
-e 's|~/.profile|~/.profile|g' \
-e 's|~/.bashrc|~/.bashrc|g' \
-e 's|~/.bash_logout|~/.bash_logout|g' \
-e 's|~/.bash_history|~/.bash_history|g' \
-e 's|~/.inputrc|~/.inputrc|g' \
-e 's|/etc/inputrc|/etc/inputrc|g'