Idris2Doc : System.File.Permissions

System.File.Permissions

Reexports

import public System.File.Error
import public System.File.Types

Definitions

data FileMode : Type
Totality: total
Visibility: public export
Constructors:
Read : FileMode
Write : FileMode
Execute : FileMode
record Permissions : Type
  The permissions of a file, grouped by the 3 types of owners of a file.

Totality: total
Visibility: public export
Constructor: 
MkPermissions : List FileMode -> List FileMode -> List FileMode -> Permissions

Projections:
.group : Permissions -> List FileMode
.others : Permissions -> List FileMode
.user : Permissions -> List FileMode
.user : Permissions -> List FileMode
Totality: total
Visibility: public export
user : Permissions -> List FileMode
Totality: total
Visibility: public export
.group : Permissions -> List FileMode
Totality: total
Visibility: public export
group : Permissions -> List FileMode
Totality: total
Visibility: public export
.others : Permissions -> List FileMode
Totality: total
Visibility: public export
others : Permissions -> List FileMode
Totality: total
Visibility: public export
chmodRaw : HasIO io => String -> Int -> io (Either FileError ())
  Change the permissions of the file with the specified name to the given
integer representation of some permissions.
You likely want to use `chmod` and `Permissions`, or go via `mkMode`
instead of using this.

@ fname the name of the file whose permissions to change
@ p the integer representation of the permissions to set

Totality: total
Visibility: export
chmod : HasIO io => String -> Permissions -> io (Either FileError ())
  Change the permissions of the file with the specified name to the
permissions in the given `Permissions` record.

@ fname the name of the file whose permissions to change
@ p a `Permissions` record containing the permissions to set

Totality: total
Visibility: export