src/Pure/General/file.ML
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 *)