mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-02 00:27:34 +03:00
da2ad89252
Better default permissions for created directories |
||
---|---|---|
.. | ||
windows | ||
.gitignore | ||
getline.c | ||
getline.h | ||
idris_buffer.c | ||
idris_buffer.h | ||
idris_directory.c | ||
idris_directory.h | ||
idris_file.c | ||
idris_file.h | ||
idris_net.c | ||
idris_net.h | ||
idris_support.c | ||
idris_support.h | ||
idris_term.c | ||
idris_term.h | ||
Makefile |