BEGIN {
      char x[ 128 ];
      y=1; }

/' /
   {
   if (y==1)
      {
      x=$1;
      y=0;
      }
   else
      x=substr($1,2);

   if (x=="File")
      {
      printf("%s\n",substr($2,3));
      }
   }

END   {}