Enhance the helper printf function for machine readable output to always
flush after each string: this way, readers of the machine readable
stream can get the output as soon as it is outputted.
---
common/mltools/tools_utils.ml | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/common/mltools/tools_utils.ml b/common/mltools/tools_utils.ml
index 5a35708cd..ade4cb37f 100644
--- a/common/mltools/tools_utils.ml
+++ b/common/mltools/tools_utils.ml
@@ -59,7 +59,11 @@ let machine_readable () =
| None -> None
| Some chan ->
let pr fs =
- ksprintf (output_string chan) fs
+ let out s =
+ output_string chan s;
+ flush chan
+ in
+ ksprintf out fs
in
Some { pr }
--
2.20.1