; a string with end-of-file
  "