# Copyright (c) P.J.Gawthrop 1998

###############################################################
## Version control history
###############################################################
## $Id$
## $Log$
# Revision 1.1  1998/01/06  13:48:23  peterg
# Initial revision
#
###############################################################

old_name=$1
new_name=$2
extension=$3

if ls $old_name$extension > /dev/null 2>&1 
then
    echo Renaming $old_name$extension to $new_name$extension
    sed "s/$old_name/$new_name/g" <$old_name$extension >$new_name$extension
fi
    then
	echo Renaming $old_name$extension to $new_name$extension
	sed "s/$old_name/$new_name/g" <$old_name$extension >$new_name$extension

	rm -f $old_name$extension
    fi