static void
write_ppm(const char *filename, const GLubyte *buffer, int width, int height)
{
  int i, x, y;
  const GLubyte *ptr = buffer;
  fprintf(stdout,"P6\n");
  fprintf(stdout,"%i %i\n", width,height);
  fprintf(stdout,"255\n");
  for (y=height-1; y>=0; y--) {
     for (x=0; x<width; x++) {
        i = (y*width + x) * 4;
        fputc(ptr[i], stdout);   /* write red */
        fputc(ptr[i+1], stdout); /* write green */
        fputc(ptr[i+2], stdout); /* write blue */
     }
  }
}