aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-02-12 18:52:09 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-02-12 18:52:09 +0100
commitde8888e28ad793511ba2e2969516325b0be44330 (patch)
treef910699eb3afb1f2b1835a01e8529c48c950b861 /tools/coqdep.ml
parent9daec838c8896e7c1048b42d01eba0c71c912f00 (diff)
Revert "Using same code for browsing physical directories in coqtop and coqdep."
(Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r--tools/coqdep.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 57c9e82f2..2e0cce6e5 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -9,7 +9,6 @@
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
@@ -462,7 +461,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 -> Systemdirs.exclude_directory r; parse ll
+ | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll
| "-exclude-dir" :: [] -> usage ()
| "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
| "-coqlib" :: [] -> usage ()