diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-06-07 17:44:54 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-06-07 17:44:54 +0200 |
| commit | 9169e5ffbf5d55d09dfc91bcf6c73f71c451387c (patch) | |
| tree | 4d817278cd91a1c38556abdb44946fd24127ffc6 /checker/checker.ml | |
| parent | 9e9c7ce7ab325a194654c3cbc1e1bf4e276ba5b7 (diff) | |
Do not use COQLIBS for the validate rule produced by coq_makefile (bug #4693).
The COQLIBS variable contains some -Q and -I options, which are not
supported by the checker. So this commit introduces a COQCHKLIBS variable
that contains the proper options for coqchk. For the sake of homogeneity,
the COQDOCLIBS variable is also preprocessed in the same way. This means
that both variables have the same value, but they are kept separate in
case the user would like to override one and not the other.
This commit also removes some deprecated options from "coqchk --help".
They are not removed from coqchk itself to preserve backward compatibility
in the branch.
An open question is whether coqchk should support dummy options such as -Q
(interpreted as -R) or -I (ignored).
Diffstat (limited to 'checker/checker.ml')
| -rw-r--r-- | checker/checker.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index 825fb4dc7..da3e3a5fc 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -179,10 +179,7 @@ let print_usage_channel co command = output_string co command; output_string co "coqchk options are:\n"; output_string co -" -I dir -as coqdir map physical dir to logical coqdir\ -\n -I dir map directory dir to the empty logical path\ -\n -include dir (idem)\ -\n -R dir coqdir recursively map physical dir to logical coqdir\ +" -R dir coqdir map physical dir to logical coqdir\ \n\ \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ |