diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2013-12-20 16:59:59 +0100 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2013-12-20 17:27:20 +0100 |
| commit | a665fd808b7fdaa11f84b35a87e0b8066cce1eda (patch) | |
| tree | 2b4d5585bdb4b258fdad6f08af5b73bb9408e4a5 /tools/coqdep.ml | |
| parent | ca1305a0187653edcf63e46b84c65130ac78d117 (diff) | |
Coqdep always uses / as dir_sep
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 16e5bbde8..8a514f7f4 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -184,7 +184,9 @@ let rec parse = function | "-coqlib" :: [] -> usage () | "-suffix" :: s :: ll -> suffixe := s ; parse ll | "-suffix" :: [] -> usage () - | "-slash" :: ll -> option_slash := true; parse ll + | "-slash" :: ll -> + Printf.eprintf "warning: option -slash has no effect and is deprecated."; + parse ll | ("-h"|"--help"|"-help") :: _ -> usage () | f :: ll -> treat_file None f; parse ll | [] -> () |