aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-07-16 15:26:59 +0200
committerEmilio Jesus Gallego Arias2020-07-16 15:26:59 +0200
commitf54bc666c62ad9a66067cb486816cdfc68c2946d (patch)
tree3e6b02e8874778411765c161384b2bf6dc25b12c /dev
parent3eccf67b2e4aed36fc6935900167b19bcf6dffde (diff)
parente52f070515833634f7a52e3440be02229e71d4fb (diff)
Merge PR #12677: Fix #12513: coq no longer reports mismatched version numbers.
Reviewed-by: ejgallego Reviewed-by: gares
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions