/* copy: copia una linea en otra */

void copy (void)
{
  int i;
  extern char line[], longest[];
  
  i=0;
  while((longest[i] = line[i])!='\0')
    i++;
}