#! /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|' \
-e 's|/bin/bash|/bin/bash|' \
-e 's|/etc/profile|/etc/profile|' \
-e 's|~/.bash_profile|~/.bash_profile|' \
-e 's|~/.bash_login|~/.bash_login|' \
-e 's|~/.profile|~/.profile|' \
-e 's|~/.bashrc|~/.bashrc|' \
-e 's|~/.bash_logout|~/.bash_logout|' \
-e 's|~/.bash_history|~/.bash_history|' \
-e 's|~/.inputrc|~/.inputrc|' \
-e 's|/etc/inputrc|/etc/inputrc|'