diff options
Diffstat (limited to 'portal/tcp/portal.ml')
| -rw-r--r-- | portal/tcp/portal.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/portal/tcp/portal.ml b/portal/tcp/portal.ml index 207bd91..f01e6ad 100644 --- a/portal/tcp/portal.ml +++ b/portal/tcp/portal.ml @@ -104,8 +104,14 @@ let socket_to_stream (sock : socket) = let chomp c = Lwt_bytes.set send_buffer !send_pos c; incr send_pos; - if !send_pos >= 1024 || c = '>' + if !send_pos >= 1024 then flush_buffer () + else if c = '>' + then + (* flush_buffer is idempotent, so we schedule to do it after other computations + happened. This means it won't take busy time, and it will flush "after", e.g. + when it's full of more interesting stuff. *) + Lwt.async (fun () -> Lwt.pause () >>= flush_buffer) |> Lwt.return else Lwt.return_unit in let close_sock = match sock with |