| changeset 70993 | 2e610951f79a |
| parent 69848 | bf2cd27714fb |
| child 73558 | a5d1d1e2f109 |
--- a/src/Pure/PIDE/byte_message.ML Sat Nov 02 12:11:00 2019 +0100 +++ b/src/Pure/PIDE/byte_message.ML Sat Nov 02 12:32:38 2019 +0100 @@ -23,7 +23,7 @@ (* output operations *) -fun write stream = List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)); +fun write stream = List.app (File.output stream); fun flush stream = ignore (try BinIO.flushOut stream);