#include <stdio.h>


grow_buffer (ppc, size)
     char **ppc;
     int size;
{
      
  *ppc = realloc (*ppc, size);
  if (*ppc == NULL)
    {
      fprintf (stderr, "Error in growing buffer to size %d\n", size);
      exit (1);
    }
}