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