mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 20:23:11 +03:00
update refc/buffer to check how many bytes have been read
This commit is contained in:
parent
35a84e505d
commit
f137d96cd6
@ -88,6 +88,8 @@
|
||||
* Deprecates `base`'s `Data.Nat.Order.decideLTE` in favor of `Data.Nat.isLTE`.
|
||||
* Removes `base`'s deprecated `System.Directory.dirEntry`. Use `nextDirEntry` instead.
|
||||
* Removes `base`'s deprecated `Data.String.fastAppend`. Use `fastConcat` instead.
|
||||
* `System.File.Buffer.readBufferData` now returns the number of bytes that have
|
||||
been read into the buffer.
|
||||
|
||||
#### Contrib
|
||||
|
||||
|
@ -38,7 +38,8 @@ main = do
|
||||
| Nothing => pure ()
|
||||
Right f <- openFile "testRead.buf" Read
|
||||
| Left err => put $ pure err
|
||||
Right ok <- readBufferData f readBuf 0 8
|
||||
Right 8 <- readBufferData f readBuf 0 8
|
||||
| Right size => put $ pure "\{show size} bytes have been read, 8 expected"
|
||||
| Left err => put $ pure err
|
||||
put $ bufferData readBuf
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user