Parcourir la source

[server] flush stdout before writing results to socket

Simon Krajewski il y a 3 ans
Parent
commit
6212d7c68d
1 fichiers modifiés avec 1 ajouts et 0 suppressions
  1. 1 0
      src/compiler/server.ml

+ 1 - 0
src/compiler/server.ml

@@ -566,6 +566,7 @@ let mk_length_prefixed_communication allow_nonblock chin chout =
 	let write = Buffer.add_string bout in
 
 	let close = fun() ->
+		flush stdout;
 		IO.write_i32 chout (Buffer.length bout);
 		IO.nwrite_string chout (Buffer.contents bout);
 		IO.flush chout