On Dec 15, 2007, at 12:28 AM, Matthew Fluet wrote: > * drop extra "Out of memory." messages Any reason? I admit it's not so nice for end-users to see these hints, but it could help developers.