aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-02-22 11:52:30 +0100
committerEmilio Jesus Gallego Arias2019-02-22 11:52:30 +0100
commitfa3a97426013cf940cd25abde43c0191766218b1 (patch)
tree9a007accd6feef4a852610dbc6095f5e5d68cd59 /tools
parent5f7bb95b6532a6983a2d1880aa531e4e4dd6568d (diff)
parent2abf8037772ee1bb9fbfa255800222663daf18e5 (diff)
Merge PR #9614: Fix #9613 use -coqlib when invoking coqchk
Reviewed-by: ejgallego
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions