src/Pure/ML-Systems/polyml.ML
changeset 54342 fbcaa9f08879
parent 53709 84522727f9d3
child 54717 42c209a6c225
--- a/src/Pure/ML-Systems/polyml.ML	Wed Oct 16 12:04:38 2013 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Oct 16 12:14:35 2013 +0200
@@ -51,6 +51,8 @@
 val raw_explode = SML90.explode;
 val implode = SML90.implode;
 
+val io_buffer_size = 4096;
+
 fun quit () = exit 0;