@@ -263,6 +263,13 @@ execApp env ctxt (EP _ fp _) (_:fn:_:handle:_:rest)
263263 "The argument to idris_readStr should be a handle, but it was " ++
264264 show handle ++
265265 ". Are all cases covered?"
266+execApp env ctxt (EP _ fp _) (_:fn:_:rest)
267+ | fp == mkfprim,
268+ Just (FFun "getchar" _ _) <- foreignFromTT fn
269+ = do -- The C API returns an Int which Idris library code
270+ -- converts; thus, we must make an int here.
271+ ch <- execIO $ fmap (ioWrap . EConstant . I . fromEnum) getChar
272+ execApp env ctxt ch rest
266273execApp env ctxt (EP _ fp _) (_:fn:rest)
267274 | fp == mkfprim,
268275 Just (FFun "idris_time" _ _) <- foreignFromTT fn