diff options
| author | Emilio Jesus Gallego Arias | 2015-12-04 19:25:08 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-12-09 14:58:36 +0100 |
| commit | ce9e7c2a842d7ec7734b58af64de9283de963e37 (patch) | |
| tree | 93dcdcbff81fc5f72390e917876a22701fe0b2ee /doc | |
| parent | 36cbe8fa3bd20469b45b299f66e88e03768a81af (diff) | |
Replace Unix.readdir by Sys.readdir in dir cache.
This makes the function sightly more portable.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions