aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Courtieu2015-11-06 17:04:24 +0100
committerPierre Courtieu2015-11-06 18:55:36 +0100
commita8b248096e5120f58157b0fc3bd06ca07118a8ab (patch)
tree83d2ba588e3ffcf0b7223bad42866ce623ac85aa
parent76bc7f9d164c20583c6561127bf36e7247a37c6b (diff)
Fixing #4406 coqdep: No recursive search of ml (-I).
-rw-r--r--tools/coqdep_common.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index c111137571..ca42c99470 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -548,7 +548,7 @@ let add_rec_dir add_file phys_dir log_dir =
(** -I semantic: do not go in subdirs. *)
let add_caml_dir phys_dir =
- handle_unix_error (add_directory true add_caml_known phys_dir) []
+ handle_unix_error (add_directory false add_caml_known phys_dir) []
let rec treat_file old_dirname old_name =