pool allocator changes and delete[] void*

[Gerald Pfeifer]

I'm afraid the recent pool allocator changes are causing troubles (or
at least tons of warnings):

   /gcc-current/bin/../lib/gcc/$platform/3.4.0/../../../../
   include/c++/3.4.0/ext/pool_allocator.h:320:
   warning: deleting `void*' is undefined

The code in question is:

 315 template<bool __threads, int __inst>
 316   void
 317   __pool_alloc<__threads, __inst>::deallocate(void* __p, size_t __n)
 318   {
 319      if ((__n > (size_t) _S_max_bytes) || (_S_force_new > 0))
 320        delete [] __p;

Gerald