At Mon, 29 Jul 2002 09:22:15 +0000 (UTC), "Richard Sandiford" wrote: > > Any reason you think the flag _shouldn't_ be checked in both places? > > No, sounds like a good idea. OK, Eric approved them off-list, and I checked them in. cgd