max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: speedcenter: reduce number of runs for "fast" benchmarks from 10 to 3 (#5009)

Browse source
This commit is contained in:
Sebastian Ullrich 2024-08-13 11:06:06 +02:00 • committed by GitHub
parent 5bc6496a7c
commit 041b80a4f5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/bench/speedcenter.yaml
View file

@ -255,13 +255,13 @@ run:
max_block_time: '-1'
# Maximum number of benchmarking runs
max_runs: 10
max_runs: 3
# Maximum time the whole benchmarking should take, -1 == no timeout, supports normal time span expressions
max_time: '-1'
# Minimum number of benchmarking runs
min_runs: 10
min_runs: 3
# Output file for the benchmarking results
out: run_output.yaml