diff options
| author | Guillaume Melquiond | 2016-06-07 17:44:54 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-06-07 17:44:54 +0200 |
| commit | 9169e5ffbf5d55d09dfc91bcf6c73f71c451387c (patch) | |
| tree | 4d817278cd91a1c38556abdb44946fd24127ffc6 /interp | |
| 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 'interp')
0 files changed, 0 insertions, 0 deletions
