diff options
| author | Hendrik Tews | 2021-03-28 22:06:03 +0200 |
|---|---|---|
| committer | Hendrik Tews | 2021-04-12 21:31:12 +0200 |
| commit | e1793962bebf1401026ed961ecc15b7eb60d57f5 (patch) | |
| tree | de4f45d46c7b226fecea6194be5a53b8b648ffbd /tools/coqdep.ml | |
| parent | ad34e3a7703d326268bab203864aa84ad3718c2c (diff) | |
[coqdep] error on non-existent and unreadable files
Print an error message and return non-zero status for
non-existing or unreadable files. Unknown options produce a
warning and are otherwise ignored.
Fixes #14023
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index f1dbac889b..199fc4225d 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -34,7 +34,8 @@ let usage () = eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; - eprintf " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE."; + eprintf " -noinit : currently no effect\n"; + eprintf " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE.\n"; eprintf " -I dir : add (non recursively) dir to ocaml path\n"; eprintf " -R dir logname : add and import dir recursively to coq load path under logical name logname\n"; eprintf " -Q dir logname : add (recursively) and open (non recursively) dir to coq load path under logical name logname\n"; @@ -64,6 +65,7 @@ let rec parse = function | "-sort" :: ll -> option_sort := true; parse ll | "-vos" :: ll -> write_vos := true; parse ll | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll + | "-noinit" :: ll -> (* do nothing *) parse ll | "-f" :: f :: ll -> treat_coqproject f; parse ll | "-I" :: r :: ll -> add_caml_dir r; parse ll | "-I" :: [] -> usage () @@ -80,6 +82,8 @@ let rec parse = function | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll | ("-h"|"--help"|"-help") :: _ -> usage () + | opt :: ll when String.length opt > 0 && opt.[0] = '-' -> + coqdep_warning "unknown option %s" opt; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () |