From 95e8234b7a3e3850710a18d26f6dd561497e25d0 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 18 Apr 2013 16:56:05 +0000 Subject: Coqdep: add an -exclude-dir option (wish mentionned in #3025) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16431 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tools/coqdep.ml | 13 ++++++++----- tools/coqdep_boot.ml | 2 +- tools/coqdep_common.ml | 16 ++++++++++------ tools/coqdep_common.mli | 3 ++- 4 files changed, 21 insertions(+), 13 deletions(-) (limited to 'tools') diff --git a/tools/coqdep.ml b/tools/coqdep.ml index a8c108f4e..f296594d1 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -157,9 +157,10 @@ let declare_dependencies () = (List.rev !vAccu) let usage () = - eprintf - "[ usage: coqdep [-w] [-I dir] [-R dir coqdir] [-coqlib dir] [-c] [-i] [-D] + ]\n"; - flush stderr; + eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-R dir coqdir] +\n"; + eprintf " extra options:\n"; + eprintf " -coqlib dir : set the coq standard library directory\n"; + eprintf " -exclude-dir f : skip subdirectories named f during -R search\n"; exit 1 let rec parse = function @@ -177,9 +178,11 @@ let rec parse = function | "-R" :: r :: "-as" :: [] -> usage () | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll | "-R" :: ([] | [_]) -> usage () - | "-coqlib" :: (r :: ll) -> Flags.coqlib_spec := true; Flags.coqlib := 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 () - | "-suffix" :: (s :: ll) -> suffixe := s ; parse ll + | "-suffix" :: s :: ll -> suffixe := s ; parse ll | "-suffix" :: [] -> usage () | "-slash" :: ll -> option_slash := true; parse ll | ("-h"|"--help"|"-help") :: _ -> usage () diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 19aba41d3..15fcdc600 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -26,7 +26,7 @@ let rec parse = function (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) add_dir add_known r []; - norecdir_list:=r::!norecdir_list; + norec_dirs:=r::!norec_dirs; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index e8d189ad9..41b026c43 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -26,7 +26,8 @@ let option_slash = ref false let option_natdynlk = ref true let option_mldep = ref None -let norecdir_list = ref ([]:string list) +let norec_dirs = ref ([] : string list) +let norec_dirnames = ref ["CVS"; "_darcs"] let suffixe = ref ".vo" @@ -439,14 +440,17 @@ let rec add_directory recur add_file phys_dir log_dir = try while true do let f = readdir dirh in - (* we avoid . .. and all hidden files and subdirs (e.g. .svn, _darcs) *) - if f.[0] <> '.' && f.[0] <> '_' then + (* we avoid all files and subdirs starting by '.' (e.g. .svn), + plus CVS and _darcs and any subdirs given via -exclude-dirs *) + if f.[0] <> '.' then let phys_f = if phys_dir = "." then f else phys_dir//f in match try (stat phys_f).st_kind with _ -> S_BLK with | S_DIR when recur -> - if List.mem phys_f !norecdir_list then () - else - add_directory recur add_file phys_f (log_dir@[f]) + if List.mem f !norec_dirnames then () + else + if List.mem phys_f !norec_dirs then () + else + add_directory recur add_file phys_f (log_dir@[f]) | S_REG -> add_file phys_dir log_dir f | _ -> () done diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index afc171cbc..d9ca3ca81 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -11,7 +11,8 @@ val option_noglob : bool ref val option_slash : bool ref val option_natdynlk : bool ref val option_mldep : string option ref -val norecdir_list : string list ref +val norec_dirs : string list ref +val norec_dirnames : string list ref val suffixe : string ref type dir = string option val ( // ) : string -> string -> string -- cgit v1.2.3