aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorGuillaume Melquiond2016-06-07 17:44:54 +0200
committerGuillaume Melquiond2016-06-07 17:44:54 +0200
commit9169e5ffbf5d55d09dfc91bcf6c73f71c451387c (patch)
tree4d817278cd91a1c38556abdb44946fd24127ffc6 /interp
parent9e9c7ce7ab325a194654c3cbc1e1bf4e276ba5b7 (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