Re: Problem with directory name in CVS checkout.