As demanded by @athei to run benchmarks via CI. Somehow I was not able to push a PR without commits. --------- Co-authored-by: command-bot <>