| changeset 70998 | 7926d2fc3c4c |
| parent 70292 | bc9d02f916c4 |
| child 72278 | 199dc903131b |
--- a/src/Pure/General/file.ML Sat Nov 02 13:25:58 2019 +0100 +++ b/src/Pure/General/file.ML Sat Nov 02 13:37:15 2019 +0100 @@ -165,7 +165,7 @@ fun append path txt = append_list path [txt]; fun generate path txt = if try read path = SOME txt then () else write path txt; -fun write_buffer path buf = open_output (Buffer.output buf) path; +fun write_buffer path buf = open_output (Buffer.output buf o output) path; (* eq *)