aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-02-20 23:22:20 +0100
committerGaëtan Gilbert2019-02-21 12:43:17 +0100
commit2abf8037772ee1bb9fbfa255800222663daf18e5 (patch)
treec605450f5a0e8534e51f9d11e396d20c46e06e2a /tools
parent924468eb648750bf2cbb6de0b1c8f7a2960f0bf5 (diff)
Fix #9613 use -coqlib when invoking coqchk
In passing add -coqlib to coqchk's usage message.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions