No specific user configuration
[platform/upstream/bash.git] / doc / infopost.sh
1 #! /bin/sh
2 #
3 # Some of these should really be done by options to makeinfo or by
4 # using @setfilename, but this way we can have both bashref.info and
5 # bash.info (for installing)
6 #
7
8 sed -e 's|bashref.info|bash.info|g'