Idris2/tests/base/system_directory/ReadDir.idr

import System
import System.Directory

panic : String -> IO a
panic s = do putStrLn s
             exitFailure

main : IO ()
main = do Right ["a"] <- listDir "dir"
            | Left e => panic (show e)
            | Right x => panic ("wrong entries: " ++ (show x))
          pure ()
System.Directory.nextDirEntry * add `nextDirEntry` which returns `Maybe String`, so `Nothing` on the end of directory unlike `dirEntry` which returns unspecified error on the end of directory * `dirEntry` is deprecated now, but not removed because compiler depends on it * native implementation of `dirEntry` is patched to explicitly reset `errno` before the `readdir` call: without it end of directory and error were indistinguishable * test added 2021-07-16 20:33:48 +03:00			`import System`
			`import System.Directory`

			`panic : String -> IO a`
			`panic s = do putStrLn s`
			`exitFailure`

			`main : IO ()`
System.Directory.listDir This function is what users want 99.9% of time. 2021-07-16 22:13:59 +03:00			`main = do Right ["a"] <- listDir "dir"`
System.Directory.nextDirEntry * add `nextDirEntry` which returns `Maybe String`, so `Nothing` on the end of directory unlike `dirEntry` which returns unspecified error on the end of directory * `dirEntry` is deprecated now, but not removed because compiler depends on it * native implementation of `dirEntry` is patched to explicitly reset `errno` before the `readdir` call: without it end of directory and error were indistinguishable * test added 2021-07-16 20:33:48 +03:00			`\| Left e => panic (show e)`
System.Directory.listDir This function is what users want 99.9% of time. 2021-07-16 22:13:59 +03:00			`\| Right x => panic ("wrong entries: " ++ (show x))`
System.Directory.nextDirEntry * add `nextDirEntry` which returns `Maybe String`, so `Nothing` on the end of directory unlike `dirEntry` which returns unspecified error on the end of directory * `dirEntry` is deprecated now, but not removed because compiler depends on it * native implementation of `dirEntry` is patched to explicitly reset `errno` before the `readdir` call: without it end of directory and error were indistinguishable * test added 2021-07-16 20:33:48 +03:00			`pure ()`