aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-03-31 21:07:51 -0400
committerEmilio Jesus Gallego Arias2020-03-31 21:07:51 -0400
commitdc723c2aa614e6b31ef5a4c9764ff92c0860880e (patch)
tree444bd2b314fac62e292e21abd43a08fd4eda4f33 /plugins
parent04af77a6b138bb139751053d63651f7187ea9952 (diff)
parentb3513cb3843a0fda58cf0e17ff21e58112e3dae8 (diff)
Merge PR #11933: Fix calling test suite makefile with a dune built coq
Reviewed-by: ejgallego
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions