On Monday, 25 March 2019 14:31:18 CET Richard W.M. Jones wrote:
> On Fri, Mar 22, 2019 at 04:33:41PM +0100, Pino Toscano wrote:
> > 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
On Fri, Mar 22, 2019 at 04:33:41PM +0100, Pino Toscano wrote:
> 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.m
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
