On Mon, Nov 10, 2008 at 04:27:58PM +0000, David Holland wrote: > I think so; I'm not sure if it matters enough to be worth the hassle > of "renaming" in CVS, though. Done - wasn't so much hassle. Thomas