Idris2Doc : System.File.Permissions

System.File.Permissions

Reexports

importpublic System.File.Error
importpublic System.File.Types

Definitions

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

Totality: total
Visibility: public export
Constructor: 
MkPermissions : ListFileMode->ListFileMode->ListFileMode->Permissions

Projections:
.group : Permissions->ListFileMode
.others : Permissions->ListFileMode
.user : Permissions->ListFileMode
.user : Permissions->ListFileMode
Totality: total
Visibility: public export
user : Permissions->ListFileMode
Totality: total
Visibility: public export
.group : Permissions->ListFileMode
Totality: total
Visibility: public export
group : Permissions->ListFileMode
Totality: total
Visibility: public export
.others : Permissions->ListFileMode
Totality: total
Visibility: public export
others : Permissions->ListFileMode
Totality: total
Visibility: public export
chmodRaw : HasIOio=>String->Int->io (EitherFileError ())
  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 : HasIOio=>String->Permissions->io (EitherFileError ())
  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