#define RAMSEY_WIDTH 1000
#define RAMSEY_HEIGHT 1000
unsigned char rgb[RAMSEY_WIDTH*RAMSEY_HEIGHT*3];
void get_rgb()
{
  glReadBuffer(GL_FRONT);
  glReadPixels(0,0,RAMSEY_WIDTH,RAMSEY_HEIGHT,GL_RGB,GL_UNSIGNED_BYTE,rgb);
}

void outputp3(char *filename)
{

  FILE *f;
  f = fopen(filename,"w");
  if(!f) { printf("Can't open file \"%s\"\n",filename); return; }
  fprintf(f,"P3\n%d %d\n%d\n", RAMSEY_WIDTH,RAMSEY_HEIGHT,256);
  for(int i = 0; i < RAMSEY_WIDTH*RAMSEY_HEIGHT; i++)
    fprintf(f,"%d %d %d   ",(int)rgb[i*3],
	    (int)rgb[i*3+1], (int)rgb[i*3+2]);
  fclose(f);
  printf("Width = %d  and Height = %d\n",RAMSEY_WIDTH,RAMSEY_HEIGHT);
  printf("Output color buffer to \"%s\"\n",filename);

}