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 /tools/coqdep.ml | |
| 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 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 2e0cce6e5..57c9e82f2 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -9,6 +9,7 @@ open Printf open Coqdep_lexer open Coqdep_common +open Systemdirs (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot]) are now in [Coqdep_common]. The code that remains here concerns @@ -461,7 +462,7 @@ let rec parse = function | "-R" :: ([] | [_]) -> usage () | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll - | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll + | "-exclude-dir" :: r :: ll -> Systemdirs.exclude_directory r; parse ll | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () |