diff options
| author | Emilio Jesus Gallego Arias | 2020-07-02 15:50:31 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-02 15:50:31 +0200 |
| commit | ce1d4079a13c0512a85a1813101e9393d8d28a26 (patch) | |
| tree | 77e1e0558a4d2246be961fd0c987d6fde66e977e | |
| parent | a1835c755f07b2199d122632360a5d236cd9984e (diff) | |
| parent | 01128e34caee5be26cde9efede40495874fc34f3 (diff) | |
Merge PR #12614: Cleanup mentions of -as in coqdep usage message
Reviewed-by: ejgallego
| -rw-r--r-- | tools/coqdep.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 20ffdfe81d..2177da0c75 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -35,9 +35,7 @@ let usage () = 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 " -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n"; eprintf " -I dir : add (non recursively) dir to ocaml path\n"; - eprintf " -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *) 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"; eprintf " -vos : also output dependencies about .vos files\n"; |