mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-08-16 19:30:32 +03:00
Some directory file function renamings
This allows us to build Idris2 proper again
This commit is contained in:
parent
e2ef9e05eb
commit
a5c9ce9306
@ -1,6 +1,6 @@
|
|||||||
##### Options which a user might set before building go here #####
|
##### Options which a user might set before building go here #####
|
||||||
|
|
||||||
PREFIX ?= $(HOME)/.idris2
|
PREFIX ?= $(HOME)/.idris2boot
|
||||||
|
|
||||||
# Add any optimisation/profiling flags for C here (e.g. -O2)
|
# Add any optimisation/profiling flags for C here (e.g. -O2)
|
||||||
OPT =
|
OPT =
|
||||||
|
@ -71,16 +71,16 @@ currentDir
|
|||||||
else pure (Just (prim__getString res))
|
else pure (Just (prim__getString res))
|
||||||
|
|
||||||
export
|
export
|
||||||
dirOpen : String -> IO (Either FileError Directory)
|
openDir : String -> IO (Either FileError Directory)
|
||||||
dirOpen d
|
openDir d
|
||||||
= do res <- primIO (prim_openDir d)
|
= do res <- primIO (prim_openDir d)
|
||||||
if prim__nullAnyPtr res /= 0
|
if prim__nullAnyPtr res /= 0
|
||||||
then returnError
|
then returnError
|
||||||
else ok (MkDir res)
|
else ok (MkDir res)
|
||||||
|
|
||||||
export
|
export
|
||||||
dirClose : Directory -> IO ()
|
closeDir : Directory -> IO ()
|
||||||
dirClose (MkDir d) = primIO (prim_closeDir d)
|
closeDir (MkDir d) = primIO (prim_closeDir d)
|
||||||
|
|
||||||
export
|
export
|
||||||
dirEntry : Directory -> IO (Either FileError String)
|
dirEntry : Directory -> IO (Either FileError String)
|
||||||
|
@ -210,8 +210,8 @@ fileStatusTime (FHandle f)
|
|||||||
else returnError
|
else returnError
|
||||||
|
|
||||||
export
|
export
|
||||||
fileRemove : String -> IO (Either FileError ())
|
removeFile : String -> IO (Either FileError ())
|
||||||
fileRemove fname
|
removeFile fname
|
||||||
= do res <- primIO (prim__fileRemove fname)
|
= do res <- primIO (prim__fileRemove fname)
|
||||||
if res == 0
|
if res == 0
|
||||||
then ok ()
|
then ok ()
|
||||||
|
Loading…
Reference in New Issue
Block a user