diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-14 10:44:22 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-14 10:44:22 +0100 |
| commit | d58957f63d36e2da41f6f839a2d94cb0db4c8125 (patch) | |
| tree | 884b79ab00b0b914a4fa2c3335491927eaf86a17 /lib/flags.ml | |
| parent | 7ae0748586fe8291f0666cce7bd39d7109471d08 (diff) | |
Remove some occurrences of Unix.opendir.
Diffstat (limited to 'lib/flags.ml')
0 files changed, 0 insertions, 0 deletions