src/Pure/General/file.ML
changeset 48911 5debc3e4fa81
parent 48446 8f611bc3650b
child 56533 cd8b6d849b6a
     1.1 --- a/src/Pure/General/file.ML	Thu Aug 23 15:44:47 2012 +0200
     1.2 +++ b/src/Pure/General/file.ML	Thu Aug 23 17:46:03 2012 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4  (*
     1.5    scalable iterator:
     1.6    . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
     1.7 -  . optional terminator at end-of-file
     1.8 +  . optional terminator at end-of-input
     1.9  *)
    1.10  fun fold_chunks terminator f path a = open_input (fn file =>
    1.11    let