On Thu, 2002-05-09 at 18:18, Tom Tromey wrote: > If nobody much cares about the memory use, then > I'll just check it in. We can always add the configure-time option > later on if it is needed. Is making this a configure time option a lot of work? AG