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