diff options
| author | Hugo Herbelin | 2015-01-31 09:09:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-02-12 17:20:35 +0100 |
| commit | 5268efdefb396267bfda0c17eb045fa2ed516b3c (patch) | |
| tree | b27a12e165d2c5b8c1b4d3171f961b8a5025bbb3 /kernel/nativecode.mli | |
| parent | e03513b7309008a45957609739bcdaf3789f3052 (diff) | |
Using same code for browsing physical directories in coqtop and coqdep.
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error).
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions