# HG changeset patch
# User wenzelm
# Date 1120639306 -7200
# Node ID c7d1c79d921cfc001331e2bb7a9f38e6f833519f
# Parent  2c1f9640b74413ef8498794ec6e02ef0d946e3b1
tuned write: use File.write_list;

diff -r 2c1f9640b744 -r c7d1c79d921c src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Wed Jul 06 10:41:45 2005 +0200
+++ b/src/Pure/General/buffer.ML	Wed Jul 06 10:41:46 2005 +0200
@@ -22,6 +22,6 @@
 val empty = Buffer [];
 fun add x (Buffer xs) = Buffer (x :: xs);
 fun content (Buffer xs) = implode (rev xs);
-fun write path buffer = File.write path (content buffer);
+fun write path (Buffer xs) = File.write_list path (rev xs);
 
 end;