Need a file renaming facility

[Dave Decot]

To move *.r.pre to *.r, do this:

	% sh
	$ for i in *.pre
	> do
	>     name=`echo $i | sed 's/.pre$//'`
	>     mv $i $name
	> done
	$ exit
        % 

Dave Decot
hpda!decot