aboutsummaryrefslogtreecommitdiff
path: root/dev/bench/gitlab.sh
AgeCommit message (Expand)Author
2021-03-07Attempt to fix the bench after coq-core splitGaëtan Gilbert
2021-02-03[bench] Re-enable coq-performance-testsJason Gross
2021-02-02Add VST to the set of default bench packages.Pierre-Marie Pédrot
2021-01-29Bench: remove broken packagesGaëtan Gilbert
2020-12-11Bench: add .log extension to .stdout/stderr filesGaëtan Gilbert
2020-11-20add perennial to benchmark suiteRalf Jung
2020-10-22Fix bench variablesGaëtan Gilbert
2020-10-19Bench: move variables to the scriptGaëtan Gilbert
2020-10-09[bench] Dump the vo size difference.Pierre-Marie Pédrot
2020-09-03[bench] Only upload some filesJason Gross
2020-09-03Merge PR #12899: [bench] Update bench script with better urls and more infoPierre-Marie Pédrot
2020-08-25Remove useless commit guessing logicJason Gross
2020-08-25[bench] Update bench script with better urls and more infoJason Gross
2020-08-24Perform a few tweaks to make the bench script work properly.Pierre-Marie Pédrot
2020-08-20Special commit to start benchmarking.Maxime Dénès