on master help sign in
Update Interactive.idr
1a59ed1Carsten König
libs/prelude/Prelude/Interactive.idr+5−5
@@ -89,13 +89,13 @@ putCharLn c = putStrLn (singleton c)
89getChar : IO Char
89getChar : IO Char
90getChar = map cast $ foreign FFI_C "getchar" (IO Int)
90getChar = map cast $ foreign FFI_C "getchar" (IO Int)
91
91
92−||| Disables buffering in both stdin and stdout
92+||| Disables buffering in both stdin and stdout:
93−||| so that output is written immediately, and never stored in the buffer
93+||| so that output is written immediately (never stored in the buffer)
94||| and the next input item is read and returned
94||| and the next input item is read and returned
95|||
95|||
96−||| this is useful to circumvent problem with IO on some Windows system
96+||| this is useful to circumvent problems with IO on some Windows systems
97−||| where stdout output sometimes is only shown after prompted input from
97+||| where stdout output right before a prompt is only shown after
98−||| stdin
98+||| the input-line from stdin is produced
99disableBuffering : IO ()
99disableBuffering : IO ()
100disableBuffering = foreign FFI_C "idris_disableBuffering" (IO ())
100disableBuffering = foreign FFI_C "idris_disableBuffering" (IO ())
101
101