#!/bin/sh
#
# $1 = full rcs file name w/path (eg. */*/*,v)
# $2 = source tree root
# $3 = destination tree root
#
# This script takes a rcs file name and make a new copy in the destination
# tree with the following rules:
#
# If $1 contains "RCS" in file name, remove it in destination file name
# This has the effect of copying a tree with ..../RCS/*.v to ....*.v
# This is a step we need to do to copy a ptools tree to cvs tree
#

# echo file name for debugging purpose
echo $1

# Check if destination directory exist, mkdir if not
DEST_DIR=$3/`dirname $1 | sed "s/RCS//" | sed "s/\.\///"`
if test ! -d $DEST_DIR
then
	mkdir -p $DEST_DIR;
	chmod g+rwx $DEST_DIR;
fi

# just copy to destination w/"RCS" removed
cp $2/$1 $DEST_DIR`basename $1`