--- a/src/Pure/General/socket_io.ML Wed Oct 16 12:04:38 2013 +0200
+++ b/src/Pure/General/socket_io.ML Wed Oct 16 12:14:35 2013 +0200
@@ -25,7 +25,7 @@
val rd =
BinPrimIO.RD {
name = name,
- chunkSize = 4096,
+ chunkSize = io_buffer_size,
readVec = SOME (fn n => Socket.recvVec (socket, n)),
readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
readVecNB = NONE,
@@ -44,7 +44,7 @@
val wr =
BinPrimIO.WR {
name = name,
- chunkSize = 4096,
+ chunkSize = io_buffer_size,
writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
writeVecNB = NONE,