Set line buffering on stdout in REPL setup
The runtime sets stdout to block buffering if it’s not connected to a terminal,
so a program piping from idris or idris --ideslave does not get responses as
they are written.
commitf59ae217eb9a3afb7b22ae034520e4f8cdfe55c5
authorMelvar Chen <Melvar.Chen@googlemail.com>
dateMon 2 Sep 2013, 17:24 (13 years ago)
parent00b401c
src/Idris/REPL.hs+2
@@ -776,6 +776,8 @@ idrisMain opts =
776776
777777 loadInputs inputs
778778
779+ liftIO $ hSetBuffering stdout LineBuffering
780+
779781 ok <- noErrors
780782 when ok $ case output of
781783 [] -> return ()