src/Pure/General/file_stream.ML
changeset 80161 fd5ed5e63a29
parent 78718 f34a451f7b5b