Indeed, you need to flush the standard output after printing there. You can do this by calling flush stdout, or indeed print_endline (which includes a flush) if you know that you want a newline anyway, or by using the %! format specifier in a printf format string (it takes no argument and just flushes), so in your code for example %s\n%! would do.
1 Like