diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-31 09:09:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-12 17:20:35 +0100 |
| commit | 5268efdefb396267bfda0c17eb045fa2ed516b3c (patch) | |
| tree | b27a12e165d2c5b8c1b4d3171f961b8a5025bbb3 /dev | |
| 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 'dev')
| -rw-r--r-- | dev/printers.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 2f78c2e91..7f8d4aad1 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -37,6 +37,7 @@ Util Bigint Dyn CUnix +Systemdirs System Envars Aux_file |