changeset 75566 | 389b193af8ae |
parent 73314 | 87403fde8cc3 |
child 75569 | f848f66a8cb7 |
--- a/src/Pure/General/file.ML Mon Jun 20 10:45:25 2022 +0200 +++ b/src/Pure/General/file.ML Mon Jun 20 16:15:07 2022 +0200 @@ -169,7 +169,8 @@ 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 o output) path; +fun write_buffer path buf = + open_output (fn file => List.app (output file) (Buffer.contents buf)) path; (* eq *)