aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r--tools/coqdep.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index a9f1b7376..1c1c1be6a 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -502,7 +502,7 @@ let coqdep () =
let user = coqlib//"user-contrib" in
if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user [];
List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s [])
- (Envars.xdg_dirs (fun x -> Feedback.msg_warning (Pp.str x)));
+ (Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (Pp.str x)));
List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath;
end;
List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;