void EchoFile(string FileName)
// Displays the contents of a text file.
{ 
   ifstream F(FileName);

   SkipBlanks(F);
   while (F.peek() != EOF)
      EchoLine(F);

   F.close();
}  // end EchoFile


void CopyTextFile(string OriginalFileName, 
                  string CopyFileName)
// ---------------------------------------------------------
// Makes a duplicate copy of a text file.
// Precondition: OriginalFileName is the name of an existing
// external text file and CopyFileName is the name of the
// text file to be created.
// Postcondition: The text file named CopyFileName is a
// duplicate of the file named OriginalFileName.
// ---------------------------------------------------------
{
   ifstream OriginalFile(OriginalFileName);  // input file
   ofstream CopyFile(CopyFileName);          // output file
   char     Ch;

   // copy characters one at a time from given file
   // to new file
   while (OriginalFile.get(Ch))
      CopyFile << Ch;

   OriginalFile.close();  // close the files
   CopyFile.close();
}  // end CopyTextFile