aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-08-27 11:25:46 +0000
committerGitHub2020-08-27 11:25:46 +0000
commit350a9ab832905dab0ff05ecb76ddb7472c271833 (patch)
tree2326e249704e380d7af605ba8c75b784171cf086 /plugins
parent1797822292e7d81fe3e5b7f76f0ddf4e29d3582c (diff)
parent0cd0d31cdd6252d02f725504bab16885cfd12906 (diff)
Merge PR #12911: Use the lite variants of performance tests in the bench default packages
Reviewed-by: JasonGross
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions